equal
deleted
inserted
replaced
49 check_file "$INFILE" |
49 check_file "$INFILE" |
50 POLY="$INFILE" |
50 POLY="$INFILE" |
51 EXIT="" |
51 EXIT="" |
52 fi |
52 fi |
53 |
53 |
|
54 ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())" |
|
55 |
54 if [ -z "$OUTFILE" ]; then |
56 if [ -z "$OUTFILE" ]; then |
55 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
57 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
56 else |
58 else |
57 if [ -z "$COMPRESS" ]; then |
59 if [ -z "$COMPRESS" ]; then |
58 COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
60 COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);" |
59 else |
61 else |
60 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
62 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);" |
61 fi |
63 fi |
62 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
64 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
63 rm -f "${OUTFILE}.o" || fail_out |
65 rm -f "${OUTFILE}.o" || fail_out |
64 fi |
66 fi |
65 |
67 |
81 |
83 |
82 if [ -n "$OUTFILE" ]; then |
84 if [ -n "$OUTFILE" ]; then |
83 if [ -e "${OUTFILE}.o" ]; then |
85 if [ -e "${OUTFILE}.o" ]; then |
84 cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out |
86 cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out |
85 rm -f "${OUTFILE}.o" |
87 rm -f "${OUTFILE}.o" |
|
88 [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE" |
86 fi |
89 fi |
87 [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
90 [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
88 fi |
91 fi |
89 |
92 |
90 exit "$RC" |
93 exit "$RC" |