diff -r c16029f41ad9 -r 5da4afa207ad lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Fri Apr 25 15:08:52 1997 +0200
+++ b/lib/scripts/run-polyml	Fri Apr 25 15:10:52 1997 +0200
@@ -4,7 +4,7 @@
 #
 # Poly/ML startup script.
 #
-# Global vars: INFILE OUTFILE COPYDB MLTEXT TERMINATE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE,
 # and from settings
 
 
@@ -31,11 +31,12 @@
 
 ## prepare databases
 
-MLINIT=""
+COPYDB=true
 
 if [ -z "$INFILE" ]; then
   INFILE="$ML_HOME/ML_dbase"
-  MLINIT="val use = PolyML.use; val exit = PolyML.exit; fun init_database () = ();"
+  MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
+  COPYDB=""
 fi
 
 if [ -z "$OUTFILE" ]; then
@@ -53,7 +54,6 @@
   echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
-  MLINIT="$MLINIT init_database ();"
 fi
 
 
@@ -62,8 +62,6 @@
 START_POLY="$POLY $ML_OPTIONS $DB"
 DB_INFO=$(ls -l "$DB")
 
-[ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT"
-
 if [ -n "$TERMINATE" ]; then
   echo "$MLTEXT" | $START_POLY
   RC=$?