equal
deleted
inserted
replaced
50 check_file "$INFILE" |
50 check_file "$INFILE" |
51 PRG="$INFILE" |
51 PRG="$INFILE" |
52 EXIT="" |
52 EXIT="" |
53 fi |
53 fi |
54 |
54 |
55 ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())" |
|
56 |
|
57 if [ -z "$OUTFILE" ]; then |
55 if [ -z "$OUTFILE" ]; then |
58 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
56 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
59 else |
57 else |
60 if [ -z "$COMPRESS" ]; then |
58 if [ -z "$COMPRESS" ]; then |
61 COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);" |
59 COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
62 else |
60 else |
63 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);" |
61 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
64 fi |
62 fi |
65 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
63 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
66 rm -f "${OUTFILE}.o" || fail_out |
64 rm -f "${OUTFILE}.o" || fail_out |
67 fi |
65 fi |
68 |
66 |