diff --git a/GMLMIP-0.1/clean.sh b/GMLMIP-0.1/clean.sh deleted file mode 100755 index 567d3219dba7ec612902c93898a29dd45a98b64f..0000000000000000000000000000000000000000 --- a/GMLMIP-0.1/clean.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/bash - -cd ./parser/ -make clean -cd .. - -cd ./formulas/ -make clean -cd .. - -cd ./rules/ -make clean -cd .. - -make clean diff --git a/GMLMIP-0.1/compile.sh b/GMLMIP-0.1/compile.sh deleted file mode 100755 index f205a8b9d5dd8c0dac40d18099ae53a4bcaaec58..0000000000000000000000000000000000000000 --- a/GMLMIP-0.1/compile.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/bash - -cd ./parser/ -make all -cd .. - -cd ./formulas/ -make all -cd .. - -cd ./rules/ -make all -cd .. - -make