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