lib/scripts/run-mosml
changeset 9789 7e5e6c47c0b5
parent 9253 fafb8dfab7f6
child 9794 2be239143d42
equal deleted inserted replaced
9788:df671fa2562a 9789:7e5e6c47c0b5
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # Moscow ML 2.00 startup script
     7 # Moscow ML 2.00 startup script
     6 #
     8 #
     7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     9 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     8 # and from settings
    10 # and from settings
    47   FEEDER_OPTS=""
    49   FEEDER_OPTS=""
    48 else
    50 else
    49   FEEDER_OPTS="-q"
    51   FEEDER_OPTS="-q"
    50 fi
    52 fi
    51 
    53 
    52 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    54 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    53   { read FPID; $ML_HOME/$MOSML $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
    55   { read FPID; "$ML_HOME/$MOSML" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    54 RC=$?
    56 RC="$?"
    55 
    57 
    56 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    58 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    57 
    59 
    58 exit $RC
    60 exit "$RC"