equal
deleted
inserted
replaced
39 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
39 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
40 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
40 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
41 |
41 |
42 for L in $ALL_LOGICS |
42 for L in $ALL_LOGICS |
43 do |
43 do |
44 ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L " |
44 ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$L " |
45 done |
45 done |
46 |
46 |
47 echo -n "Finished at "; date |
47 echo -n "Finished at "; date |
48 |
48 |
49 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
49 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |