diff -r 4deae4b33d97 -r a9c2d42937dd lib/scripts/run-poplogml
--- 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