From: Hendrik Tews Date: Wed, 12 Feb 2020 05:41:25 +0100 Subject: don't build the proof-recording version as part of the test suite --- holtest | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/holtest b/holtest index 086b40b..d5043ef 100755 --- a/holtest +++ b/holtest @@ -205,7 +205,7 @@ echo '### Loading 100/two_squares.ml'; echo 'loadt "100/two_squares.ml";;' | (ti echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time $hollight) # Build the proof-recording version of HOL - -echo '### Building proof-recording version'; -cd Proofrecording/hol_light -make clean; make hol +# ... not on Debian +# echo '### Building proof-recording version'; +# cd Proofrecording/hol_light +# make clean; make hol