equal
deleted
inserted
replaced
65 [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT" |
65 [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT" |
66 |
66 |
67 if [ -n "$TERMINATE" ]; then |
67 if [ -n "$TERMINATE" ]; then |
68 echo "$MLTEXT" | $START_POLY |
68 echo "$MLTEXT" | $START_POLY |
69 RC=$? |
69 RC=$? |
|
70 elif [ -z "$MLTEXT" ]; then |
|
71 sh -c "$ISABELLE_HOME/lib/Tools/symbolinput | $START_POLY" |
|
72 RC=$? |
70 else |
73 else |
71 { echo "$MLTEXT"; $ISABELLE_HOME/lib/Tools/symbolinput } | $START_POLY |
74 sh -c "{ echo '$MLTEXT'; $ISABELLE_HOME/lib/Tools/symbolinput; } | $START_POLY" |
72 RC=$? |
75 RC=$? |
73 fi |
76 fi |
74 |
77 |
75 NEW_DB_INFO=$(ls -l "$DB") |
78 NEW_DB_INFO=$(ls -l "$DB") |
76 [ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" |
79 [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE" |
77 |
80 |
78 exit $RC |
81 exit $RC |