1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
From: Hendrik Tews <hendrik@askra.de>
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
|
