# HG changeset patch
# User wenzelm
# Date 1127326595 -7200
# Node ID 4de614cc6509608707ec268136a04f31eb910440
# Parent  81fcc00297615a3df1a847f3fb38c7f632b8563a
updated for Isabelle2005;

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