# HG changeset patch # User wenzelm # Date 1275489778 -7200 # Node ID 344468462338bb9610004d221392b4d1533d0cbb # Parent 085cbd6a2a58c8477d60582ac5a13d14fc625cfa removed obsolete usedir -p 1 option; diff -r 085cbd6a2a58 -r 344468462338 Admin/makebin --- a/Admin/makebin Wed Jun 02 15:38:27 2010 +0200 +++ b/Admin/makebin Wed Jun 02 16:42:58 2010 +0200 @@ -87,11 +87,11 @@ cd "$ISABELLE_NAME" perl -pi \ - -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \ + -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \ etc/settings if [ -n "$DO_LIBRARY" ]; then - perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \ + perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \ etc/settings fi