equal
deleted
inserted
replaced
79 mkdir -p "$LOGDIR" |
79 mkdir -p "$LOGDIR" |
80 |
80 |
81 |
81 |
82 # run isabelle |
82 # run isabelle |
83 |
83 |
84 SECONDS=0 |
84 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
85 |
85 |
86 if [ -z "$RAW" ]; then |
86 if [ -z "$RAW" ]; then |
87 ITEM="Pure" |
87 ITEM="Pure" |
88 echo "Building $ITEM ..." |
88 echo "Building $ITEM ..." |
89 LOG="$LOGDIR/$ITEM" |
89 LOG="$LOGDIR/$ITEM" |
105 -e "use\"$COMPAT\" handle _ => exit 1;" \ |
105 -e "use\"$COMPAT\" handle _ => exit 1;" \ |
106 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
106 -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1 |
107 RC="$?" |
107 RC="$?" |
108 fi |
108 fi |
109 |
109 |
110 ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") |
110 . "$ISABELLE_HOME/lib/scripts/timestop.bash" |
111 |
111 |
112 |
112 |
113 # exit status |
113 # exit status |
114 |
114 |
115 if [ "$RC" -eq 0 ]; then |
115 if [ "$RC" -eq 0 ]; then |
116 echo "Finished $ITEM ($ELAPSED elapsed time)" |
116 echo "Finished $ITEM ($TIMES_REPORT)" |
117 gzip --force "$LOG" |
117 gzip --force "$LOG" |
118 else |
118 else |
119 echo "$ITEM FAILED" |
119 echo "$ITEM FAILED" |
120 echo "(see also $LOG)" |
120 echo "(see also $LOG)" |
121 echo; tail "$LOG"; echo |
121 echo; tail "$LOG"; echo |