Admin/makebin

--- a/Admin/makebin	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/makebin	Mon Jan 04 11:55:23 2010 +0100
@@ -88,7 +88,6 @@
 
 perl -pi \
   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
-  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
   etc/settings
 
 if [ -n "$DO_LIBRARY" ]; then