equal
deleted
inserted
replaced
40 |
40 |
41 MLTEXT="$EXIT $COMMIT $MLTEXT" |
41 MLTEXT="$EXIT $COMMIT $MLTEXT" |
42 MLEXIT="commit();" |
42 MLEXIT="commit();" |
43 |
43 |
44 if [ -z "$TERMINATE" ]; then |
44 if [ -z "$TERMINATE" ]; then |
45 FEEDER_OPTS="-s" |
45 FEEDER_OPTS="" |
46 else |
46 else |
47 FEEDER_OPTS="-q" |
47 FEEDER_OPTS="-q" |
48 fi |
48 fi |
49 |
49 |
50 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |
50 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ |