changeset 39686 | 8b9f971ace20 |
parent 38434 | 7aa0245aeede |
child 41967 | 6aa69999da8f |
--- a/Admin/isatest/isatest-makeall Fri Sep 24 15:30:30 2010 +0200 +++ b/Admin/isatest/isatest-makeall Fri Sep 24 15:37:36 2010 +0200 @@ -146,6 +146,8 @@ echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 + echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1 + if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then echo "--- cleaning up old $ISABELLE_HOME_USER" rm -rf $ISABELLE_HOME_USER