lib/scripts/run-mlworks
changeset 4433 960868c0cbdd
parent 4426 824cac1bbcfd
child 4505 4a2c872b6513
equal deleted inserted replaced
4432:a8f5293f7cbc 4433:960868c0cbdd
    40 MLEXIT="commit ();"
    40 MLEXIT="commit ();"
    41 
    41 
    42 
    42 
    43 ## run it!
    43 ## run it!
    44 
    44 
    45 START_MLWORKS="$ML_HOME/$MLWORKS $ML_OPTIONS"
    45 START_MLWORKS="$ML_HOME/$MLWORKS 2>&1 $ML_OPTIONS"
    46 
    46 
    47 if [ -n "$TERMINATE" ]; then
    47 if [ -n "$TERMINATE" ]; then
    48   sh -c "echo '$MLTEXT' '$MLEXIT' | $START_MLWORKS"
    48   sh -c "echo '$MLTEXT' '$MLEXIT' | $START_MLWORKS"
    49   RC=$?
    49   RC=$?
    50 elif [ -z "$MLTEXT" ]; then
    50 elif [ -z "$MLTEXT" ]; then
    53 else
    53 else
    54   sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS"
    54   sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; echo '$MLEXIT'; } | $START_MLWORKS"
    55   RC=$?
    55   RC=$?
    56 fi
    56 fi
    57 
    57 
    58 #fix heap file name
       
    59 [ -n "$OUTFILE" -a -n "$SUFFIX" -a -f "$OUTFILE$SUFFIX" ] \
       
    60   && mv "$OUTFILE$SUFFIX" "$OUTFILE"
       
    61 
       
    62 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    58 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    63 
    59 
    64 exit $RC
    60 exit $RC