--- a/lib/scripts/run-mlworks Thu Sep 28 14:40:38 2000 +0200
+++ b/lib/scripts/run-mlworks Thu Sep 28 14:41:48 2000 +0200
@@ -6,7 +6,7 @@
#
# MLWorks startup script (for 1.0r2 or later).
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-mosml Thu Sep 28 14:40:38 2000 +0200
+++ b/lib/scripts/run-mosml Thu Sep 28 14:41:48 2000 +0200
@@ -6,7 +6,7 @@
#
# Moscow ML 2.00 startup script
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-polyml Thu Sep 28 14:40:38 2000 +0200
+++ b/lib/scripts/run-polyml Thu Sep 28 14:41:48 2000 +0200
@@ -6,7 +6,7 @@
#
# Poly/ML startup script.
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
@@ -48,13 +48,12 @@
## prepare databases
-COPYDB=true
-
if [ -z "$INFILE" ]; then
INFILE="$ML_HOME/ML_dbase"
check_mlhome_file "$INFILE"
- COPYDB=""
MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
+else
+ COPYDB=true
fi
if [ -z "$OUTFILE" ]; then
--- a/lib/scripts/run-smlnj Thu Sep 28 14:40:38 2000 +0200
+++ b/lib/scripts/run-smlnj Thu Sep 28 14:41:48 2000 +0200
@@ -6,7 +6,7 @@
#
# SML/NJ startup script (for 110 or later).
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics
--- a/lib/scripts/run-smlnj-0.93 Thu Sep 28 14:40:38 2000 +0200
+++ b/lib/scripts/run-smlnj-0.93 Thu Sep 28 14:41:48 2000 +0200
@@ -6,7 +6,7 @@
#
# SML/NJ startup script (for 0.93).
-export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE
+export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE
## diagnostics