1.1 --- a/Admin/makebin	Mon Oct 23 22:07:08 2000 +0200
     1.2 +++ b/Admin/makebin	Mon Oct 23 22:09:21 2000 +0200
     1.3 @@ -77,7 +77,8 @@
     1.4    touch "heaps/$COMPILER/HOL-Real"
     1.5    touch "heaps/$COMPILER/ZF"
     1.6  else
     1.7 -  ./build -b -m Pure-copied Pure
     1.8 +  #FIXME for Poly/ML 3.x only ...
     1.9 +  #./build -b -m Pure-copied Pure
    1.10    ./build -b -m HOL-Real HOL
    1.11    ./build -b ZF
    1.12    rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"