--- a/lib/scripts/run-poplogml Sat Oct 08 22:39:42 2005 +0200
+++ b/lib/scripts/run-poplogml Sat Oct 08 23:05:59 2005 +0200
@@ -88,6 +88,7 @@
if [ -z "$OUTFILE" ]; then
COMMIT='fun commit () = (StdIO.output (StdIO.std_err, "Error - Database is not opened for writing.\n"); false);'
else
+ ML_OPTIONS="$ML_OPTIONS -nort"
if [ -z "$NOWRITE" ]; then
COMMIT="fun commit () = if System.make {image =\"$OUTFILE\", lock = false, share = false, banner = false, init = false} then System.restart() else true;"
else