From 5b22e118722187529d78323e1540c7bf0b9215c6 Mon Sep 17 00:00:00 2001
From: Hans-Christoph Steiner <hans@eds.org>
Date: Wed, 2 Apr 2014 18:32:41 -0400
Subject: [PATCH] make jenkins script use bash so we can use bashisms

---
 jenkins-build.sh => jenkins-build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename jenkins-build.sh => jenkins-build (99%)

diff --git a/jenkins-build.sh b/jenkins-build
similarity index 99%
rename from jenkins-build.sh
rename to jenkins-build
index ccd9492e..a5219f2f 100755
--- a/jenkins-build.sh
+++ b/jenkins-build
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
 #
 # this is the script run by the Jenkins server to run the build and tests.  Be
 # sure to always run it in its dir, i.e. ./jenkins-build.sh, otherwise it might
-- 
2.30.2