--- a/lib/scripts/run-polyml Wed Sep 22 21:21:04 2010 +0200
+++ b/lib/scripts/run-polyml Wed Sep 22 22:14:25 2010 +0200
@@ -52,17 +52,18 @@
fi
if [ -z "$OUTFILE" ]; then
- COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+ COMMIT='fun commit () = false;'
+ MLEXIT=""
else
COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
[ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+ MLEXIT="commit();"
fi
## run it!
MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
if [ -z "$TERMINATE" ]; then
FEEDER_OPTS=""