tuned messages;
authorwenzelm
Thu, 28 Sep 2006 15:30:03 +0200
changeset 20760 f8281cbf37a5
parent 20759 1cd271a4fb12
child 20761 7a6f69cf5a86
tuned messages;
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