equal
deleted
inserted
replaced
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # Poly/ML startup script. |
5 # Poly/ML startup script. |
6 # |
6 # |
7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
7 # Global vars: INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
8 # and from settings |
8 # and from settings |
9 |
9 |
10 |
10 |
11 ## diagnostics |
11 ## diagnostics |
12 |
12 |
83 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \ |
83 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \ |
84 { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; } |
84 { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; } |
85 RC=$? |
85 RC=$? |
86 |
86 |
87 NEW_DB_INFO=$(ls -l "$DB") |
87 NEW_DB_INFO=$(ls -l "$DB") |
88 [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" |
88 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" |
89 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
89 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
90 |
90 |
91 exit $RC |
91 exit $RC |