changeset 10101 | 746263fbcbfd |
parent 10097 | 1db5bd97f6a3 |
child 10113 | a1f8d7d4084b |
--- a/Admin/makebin Thu Sep 28 14:35:23 2000 +0200 +++ b/Admin/makebin Thu Sep 28 14:35:42 2000 +0200 @@ -77,6 +77,7 @@ touch "heaps/$COMPILER/HOL-Real" touch "heaps/$COMPILER/ZF" else + ./build -b -m Pure-copied Pure ./build -b -m HOL-Real HOL ./build -b ZF rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"