make jenkins script use bash so we can use bashisms

diff --git a/jenkins-build.sh b/jenkins-build
similarity index 99%
rename from jenkins-build.sh
rename to jenkins-build
index ccd9492e613f987a97eb8ee323d8296a78ef1260..a5219f2ffd5db97e8dc8cb00d7866a12608fe4f2 100755 (executable)
--- 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