| changeset 10105 | f9be78009930 |
| parent 9997 | 38598a19e701 |
| child 10555 | 2323ec838401 |
--- 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