lib/scripts/run-polyml-5.0
changeset 21711 dfac729d3066
parent 21653 219924615db6
child 21713 85722dc0fc81
--- a/lib/scripts/run-polyml-5.0	Fri Dec 08 18:22:28 2006 +0100
+++ b/lib/scripts/run-polyml-5.0	Fri Dec 08 22:17:20 2006 +0100
@@ -51,13 +51,15 @@
   EXIT=""
 fi
 
+ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
+
 if [ -z "$OUTFILE" ]; then
   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
 else
   if [ -z "$COMPRESS" ]; then
-    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
   else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   rm -f "${OUTFILE}.o" || fail_out
@@ -83,6 +85,7 @@
   if [ -e "${OUTFILE}.o" ]; then
     cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
     rm -f "${OUTFILE}.o"
+    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
   fi
   [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 fi