# HG changeset patch # User wenzelm # Date 1159450203 -7200 # Node ID f8281cbf37a559fe444fe4e93c0ab29b6ee5b715 # Parent 1cd271a4fb12b19d0cf781b2cc297378af8249f6 tuned messages; diff -r 1cd271a4fb12 -r f8281cbf37a5 lib/scripts/run-polyml-4.9.1 --- a/lib/scripts/run-polyml-4.9.1 Thu Sep 28 11:56:30 2006 +0200 +++ b/lib/scripts/run-polyml-4.9.1 Thu Sep 28 15:30:03 2006 +0200 @@ -53,9 +53,9 @@ COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' else if [ -z "$COMPRESS" ]; then - COMMIT="fun commit () = (PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" + COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" else - COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" fi [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } rm -f "${OUTFILE}.o" || fail_out