Admin/makebin
changeset 34238 b28be884edda
parent 33918 5945e023bab7
child 37286 344468462338
equal deleted inserted replaced
34237:225daff4323b 34238:b28be884edda
    86 tar xzf "$ARCHIVE_FULL"
    86 tar xzf "$ARCHIVE_FULL"
    87 cd "$ISABELLE_NAME"
    87 cd "$ISABELLE_NAME"
    88 
    88 
    89 perl -pi \
    89 perl -pi \
    90   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
    90   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
    91   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
       
    92   etc/settings
    91   etc/settings
    93 
    92 
    94 if [ -n "$DO_LIBRARY" ]; then
    93 if [ -n "$DO_LIBRARY" ]; then
    95   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \
    94   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \
    96     etc/settings
    95     etc/settings