equal
deleted
inserted
replaced
71 |
71 |
72 if [ -z "$INFILE" ]; then |
72 if [ -z "$INFILE" ]; then |
73 check_file "$ML_DBASE_PREFIX$ML_DBASE" |
73 check_file "$ML_DBASE_PREFIX$ML_DBASE" |
74 INFILE="$ML_DBASE" |
74 INFILE="$ML_DBASE" |
75 MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
75 MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
|
76 [ "$ML_SYSTEM" = polyml-4.1.3 ] && \ |
|
77 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -Smax" |
76 [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \ |
78 [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \ |
77 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
79 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
78 else |
80 else |
79 COPYDB=true |
81 COPYDB=true |
80 fi |
82 fi |
109 |
111 |
110 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
112 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
111 { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
113 { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
112 RC="$?" |
114 RC="$?" |
113 |
115 |
|
116 |
114 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null) |
117 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null) |
115 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |
118 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \ |
116 "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE" |
119 "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE" |
117 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
120 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
118 |
121 |