From e07d231b2f32755a7a37d3a70617940747eac322 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 15 Jun 2015 12:10:21 +0200 Subject: [PATCH] [jenkins] Remove unused jenkins scripts --- buildtools/jenkins/run.bat | 1 - buildtools/jenkins/runmingw.sh | 22 ---------------------- 2 files changed, 23 deletions(-) delete mode 100755 buildtools/jenkins/run.bat delete mode 100755 buildtools/jenkins/runmingw.sh diff --git a/buildtools/jenkins/run.bat b/buildtools/jenkins/run.bat deleted file mode 100755 index 16c8cd6af7..0000000000 --- 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 index 27cad0bc00..0000000000 --- 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 -- 2.20.1