changeset 10307 | 0df0bbd7e324 |
parent 10113 | a1f8d7d4084b |
child 11576 | c418146c4763 |
--- a/Admin/makebin Mon Oct 23 22:07:08 2000 +0200 +++ b/Admin/makebin Mon Oct 23 22:09:21 2000 +0200 @@ -77,7 +77,8 @@ touch "heaps/$COMPILER/HOL-Real" touch "heaps/$COMPILER/ZF" else - ./build -b -m Pure-copied Pure + #FIXME for Poly/ML 3.x only ... + #./build -b -m Pure-copied Pure ./build -b -m HOL-Real HOL ./build -b ZF rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"