Admin/makebin
changeset 37286 344468462338
parent 34238 b28be884edda
child 37340 f3492868bbfd
equal deleted inserted replaced
37285:085cbd6a2a58 37286:344468462338
    85 cd "$TMP"
    85 cd "$TMP"
    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":;' \
    91   etc/settings
    91   etc/settings
    92 
    92 
    93 if [ -n "$DO_LIBRARY" ]; then
    93 if [ -n "$DO_LIBRARY" ]; then
    94   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 -i true -d pdf -V outline=/proof,/ML":;' \
    95     etc/settings
    95     etc/settings
    96 fi
    96 fi
    97 
    97 
    98 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
    98 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
    99 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    99 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \