lib/scripts/run-smlnj
changeset 2429 747177b67670
parent 2396 721a9e01457b
child 2622 80a81a36dd81
equal deleted inserted replaced
2428:853732a26bdd 2429:747177b67670
    41 elif [ -n "$INFILE" -a ! "$INFILE" -ef "$OUTFILE" ]; then
    41 elif [ -n "$INFILE" -a ! "$INFILE" -ef "$OUTFILE" ]; then
    42   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
    42   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
    43   cp "$INFILE" "$OUTFILE" || fail_out
    43   cp "$INFILE" "$OUTFILE" || fail_out
    44 fi
    44 fi
    45 
    45 
    46 [ -n "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
    46 [ -n "$OUTFILE" -a -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out }
    47 
    47 
    48 MLTEXT="$EXIT $COMMIT $MLTEXT"
    48 MLTEXT="$EXIT $COMMIT $MLTEXT"
    49 MLEXIT="commit();"
    49 MLEXIT="commit();"
    50 
    50 
    51 
    51 
    52 ## run it!
    52 ## run it!
    53 
    53 
    54 START_SML="$ML_HOME/bin/sml $ML_OPTIONS $DB"
    54 START_SML="$ML_HOME/sml $ML_OPTIONS $DB"
    55 
    55 
    56 if [ -n "$TERMINATE" ]; then
    56 if [ -n "$TERMINATE" ]; then
    57   { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
    57   { echo "$MLTEXT"; echo "$MLEXIT" } | $START_SML
    58   RC=$?
    58   RC=$?
    59 else
    59 else