comment out Pure-copied target;
authorwenzelm
Mon, 23 Oct 2000 22:09:21 +0200
changeset 10307 0df0bbd7e324
parent 10306 b0ab988a27a9
child 10308 c50fc8023ac0
comment out Pure-copied target;
Admin/makebin
--- 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"