--- 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