| changeset 13834 | 4d50cf8ea3d7 |
| parent 13235 | c26fc3baeffc |
| child 14281 | a8c4a1e63071 |
| 13833:f8dcb1d9ea68 | 13834:4d50cf8ea3d7 |
|---|---|
47 echo -n "Finished at "; date |
47 echo -n "Finished at "; date |
48 |
48 |
49 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |
49 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |
50 echo "$ELAPSED total elapsed time" |
50 echo "$ELAPSED total elapsed time" |
51 |
51 |
52 [ "$FAIL" == "" ] || fail "Logics ${FAIL}FAILED!" |
52 [ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!" |