From 53b158e6299ce0e51cf457188012d8685e9f3bfc Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Mon, 27 Jul 2015 16:13:18 +0200
Subject: [PATCH] [jenkins] Display arguments passed to the script

---
 buildtools/jenkins/build.sh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/buildtools/jenkins/build.sh b/buildtools/jenkins/build.sh
index 1e440f5f9d..125d3ca109 100755
--- a/buildtools/jenkins/build.sh
+++ b/buildtools/jenkins/build.sh
@@ -2,8 +2,12 @@
 
 set -e
 
-build_mode="$1"
+echo "Running $0 with arguments:" >&2
+for arg in "$@"; do
+  echo "- $arg"
+done
 
+build_mode="$1"
 echo "Build mode $build_mode on $(uname -np)" >&2
 
 if test "$(uname -o)" = "Msys"; then
-- 
2.20.1