# 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