lib/scripts/run-polyml-5.0
changeset 21711 dfac729d3066
parent 21653 219924615db6
child 21713 85722dc0fc81
equal deleted inserted replaced
21710:4e4b7c801142 21711:dfac729d3066
    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"