Admin/makebin
changeset 17575 c45677c1aea0
parent 17573 4de614cc6509
child 17660 94bbe14c088e
     1.1 --- a/Admin/makebin	Wed Sep 21 20:26:45 2005 +0200
     1.2 +++ b/Admin/makebin	Wed Sep 21 21:00:57 2005 +0200
     1.3 @@ -102,11 +102,13 @@
     1.4  use_thy "HOL4";
     1.5  EOF
     1.6  
     1.7 +perl -pi \
     1.8 +  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
     1.9 +  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
    1.10 +  etc/settings
    1.11 +
    1.12  if [ -n "$DO_LIBRARY" ]; then
    1.13 -  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-i true -d pdf -V outline=/proof,/ML":' \
    1.14 -    etc/settings
    1.15 -else
    1.16 -  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 2":' \
    1.17 +  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
    1.18      etc/settings
    1.19  fi
    1.20  
    1.21 @@ -132,10 +134,8 @@
    1.22    ./build -bait
    1.23  else
    1.24    ./build -b -m HOL-Complex HOL
    1.25 +  ./build -b -m HOL4 HOL
    1.26    ./build -b ZF
    1.27 -  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
    1.28 -    etc/settings
    1.29 -  ./build -b -m HOL4 HOL
    1.30    rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
    1.31  fi
    1.32