equal
deleted
inserted
replaced
51 |
51 |
52 if [ -z "$OUTFILE" ]; then |
52 if [ -z "$OUTFILE" ]; then |
53 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
53 COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' |
54 else |
54 else |
55 if [ -z "$COMPRESS" ]; then |
55 if [ -z "$COMPRESS" ]; then |
56 COMMIT="fun commit () = (PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
56 COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
57 else |
57 else |
58 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
58 COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);" |
59 fi |
59 fi |
60 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
60 [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } |
61 rm -f "${OUTFILE}.o" || fail_out |
61 rm -f "${OUTFILE}.o" || fail_out |
62 fi |
62 fi |
63 |
63 |