[jenkins] Remove unused jenkins scripts

diff --git a/buildtools/jenkins/run.bat b/buildtools/jenkins/run.bat
deleted file mode 100755 (executable)
index 16c8cd6..0000000
--- a/buildtools/jenkins/run.bat
+++ /dev/null
@@ -1 +0,0 @@
-c:\mingw\msys\1.0\bin\sh -login .\buildtools\jenkins\runmingw.sh %1 %2

diff --git a/buildtools/jenkins/runmingw.sh b/buildtools/jenkins/runmingw.sh
deleted file mode 100755 (executable)
index 27cad0b..0000000
--- a/buildtools/jenkins/runmingw.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!c:\mingw\msys\1.0\bin\sh -login
-
-WORKSPACE=$1
-build_mode=$2
-
-rm -rf $WORKSPACE/build
-rm -rf $WORKSPACE/install
-mkdir $WORKSPACE/build
-mkdir $WORKSPACE/install
-cd $WORKSPACE/build
-
-if [ "$build_mode" = "Debug" ]
-then
-cmake -G "MSYS Makefiles" ..
-fi
-
-if [ "$build_mode" = "ModelChecker" ]
-then
-cmake -G "MSYS Makefiles" -Denable_documentation=OFF -Denable_model-checking=ON -Denable_compile_optimizations=OFF ..
-fi
-
-make