author | wenzelm |
Fri, 24 Sep 2010 15:37:36 +0200 | |
changeset 39686 | 8b9f971ace20 |
parent 39685 | d8071cddb877 |
child 39687 | 4e9b6ada3a21 |
--- 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