Admin/makebin
changeset 34238 b28be884edda
parent 33918 5945e023bab7
child 37286 344468462338
     1.1 --- a/Admin/makebin	Sun Jan 03 15:09:02 2010 +0100
     1.2 +++ b/Admin/makebin	Mon Jan 04 11:55:23 2010 +0100
     1.3 @@ -88,7 +88,6 @@
     1.4  
     1.5  perl -pi \
     1.6    -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
     1.7 -  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
     1.8    etc/settings
     1.9  
    1.10  if [ -n "$DO_LIBRARY" ]; then