more work on jenkins stuff
diff --git a/tools/jenkins/build_configuration.sh b/tools/jenkins/build_configuration.sh
new file mode 100755
index 0000000..70babb6
--- /dev/null
+++ b/tools/jenkins/build_configuration.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+EXECUTOR_NUMBER=$1
+CONFIGURATION=$2
+
+function usage() {
+ echo "Usage: $0 - Build a configuration"
+ echo ""
+ echo "$0 [EXECUTOR_NUMBER] [CONFIGURATION]"
+ exit 1
+}
+
+# Validate inputs
+if [[ "$EXECUTOR_NUMBER" = "" || "$CONFIGURATION" = "" ]]; then
+ usage
+fi
+
+# Execute configuration script
+cd configurations && ./$CONFIGURATION.sh $EXECUTOR_NUMBER $CONFIGURATION