diff -r 81fcc0029761 -r 4de614cc6509 Admin/makebin
--- a/Admin/makebin	Wed Sep 21 20:16:34 2005 +0200
+++ b/Admin/makebin	Wed Sep 21 20:16:35 2005 +0200
@@ -103,10 +103,10 @@
 EOF
 
 if [ -n "$DO_LIBRARY" ]; then
-  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf -V outline=/proof,/ML"/' \
+  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-i true -d pdf -V outline=/proof,/ML":' \
     etc/settings
 else
-  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \
+  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 2":' \
     etc/settings
 fi