lib/scripts/run-polyml
changeset 9789 7e5e6c47c0b5
parent 9765 46def28153d6
child 9977 32955afeb835
     1.1 --- a/lib/scripts/run-polyml	Fri Sep 01 17:50:36 2000 +0200
     1.2 +++ b/lib/scripts/run-polyml	Fri Sep 01 17:54:58 2000 +0200
     1.3 @@ -1,6 +1,8 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # Poly/ML startup script.
    1.11  #
    1.12 @@ -28,8 +30,8 @@
    1.13  
    1.14  ## Poly/ML programs
    1.15  
    1.16 -POLY=$ML_HOME/poly
    1.17 -DISCGARB=$ML_HOME/discgarb
    1.18 +POLY="$ML_HOME/poly"
    1.19 +DISCGARB="$ML_HOME/discgarb"
    1.20  
    1.21  check_mlhome_file "$POLY"
    1.22  check_mlhome_file "$DISCGARB"
    1.23 @@ -68,7 +70,7 @@
    1.24    DB="$OUTFILE"
    1.25  else
    1.26    [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
    1.27 -  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
    1.28 +  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
    1.29    [ -f "$OUTFILE" ] || fail_out
    1.30    DB="$OUTFILE"
    1.31  fi
    1.32 @@ -84,12 +86,12 @@
    1.33  
    1.34  DB_INFO=$(ls -l "$DB")
    1.35  
    1.36 -$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \
    1.37 -  { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; }
    1.38 -RC=$?
    1.39 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
    1.40 +  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    1.41 +RC="$?"
    1.42  
    1.43  NEW_DB_INFO=$(ls -l "$DB")
    1.44 -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB -c "$OUTFILE"
    1.45 +[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE"
    1.46  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    1.47  
    1.48 -exit $RC
    1.49 +exit "$RC"