# HG changeset patch
# User wenzelm
# Date 972331761 -7200
# Node ID 0df0bbd7e32439a9c97ad191629c88935af21158
# Parent  b0ab988a27a9ed28b8ec67e09481784b59a09e1b
comment out Pure-copied target;

diff -r b0ab988a27a9 -r 0df0bbd7e324 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"