From ddafa605946e2765389d8cf7a673bd92406bbcd7 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 24 Apr 2018 13:35:06 +0200
Subject: [PATCH] Next iteration on ci script

---
 scripts/ci-hol4.sh | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

diff --git a/scripts/ci-hol4.sh b/scripts/ci-hol4.sh
index 275e24e..739dabb 100755
--- a/scripts/ci-hol4.sh
+++ b/scripts/ci-hol4.sh
@@ -8,31 +8,23 @@ then
     sleep 5
 
     #Set HOL4 commit variable
-    HOLCOMMIT="$(cat ./.HOLCOMMIT)"
-    pushd
+    HOLCOMMIT="$(cat ./hol4/.HOLCOMMIT)"
+    pushd ./
     cd ~/
     git clone https://github.com/HOL-Theorem-Prover/HOL.git HOL4
     cd HOL4
     git checkout $HOLCOMMIT
     poly < tools/smart-configure.sml
     bin/build
+    export HOLDIR=~/HOL4/
     popd
 fi
 
 cd ./hol4
-#Run configure script to check the versions
-./configure_hol.sh
-RET=$?
 
-if [ $RET -eq 1 ];
-then
-   echo "Updating HOL4 to the latest state specified in HOLCOMMIT"
-   ./configure_hol.sh --init
-else
-    echo "Downloading CakeML"
-    git submodule init cakeml
-    git submodule update -f cakeml
-fi
+echo "Downloading CakeML"
+git submodule init cakeml
+git submodule update -f cakeml
 
 $HOLDIR/bin/Holmake -q
 
-- 
GitLab