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