From b139e510412430cb7decd58a098871f7ded9ef0c Mon Sep 17 00:00:00 2001
From: Richard van der Hoff <richard@matrix.org>
Date: Thu, 3 Mar 2016 11:38:36 +0000
Subject: [PATCH] jenkins.sh: set -x

Also move the options from the shebang line to the body of the script, so that
they take effect even if somebody explicitly runs "bash jenkins.sh"
---
 jenkins.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/jenkins.sh b/jenkins.sh
index 9646ac0b01..b826d510c9 100755
--- a/jenkins.sh
+++ b/jenkins.sh
@@ -1,4 +1,6 @@
-#!/bin/bash -eu
+#!/bin/bash
+
+set -eux
 
 : ${WORKSPACE:="$(pwd)"}