diff -r 7a06bf89c038 -r eb82ed858b84 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Thu Sep 03 14:31:04 2009 +0200 +++ b/Admin/isatest/isatest-makeall Thu Sep 03 14:40:52 2009 +0200 @@ -10,6 +10,8 @@ # max time until test is aborted (in sec) MAXTIME=28800 +PUBLISH_TEST=/home/isabelle-repository/repos/testtool/publish_test.py + ## diagnostics PRG="$(basename "$0")" @@ -120,6 +122,8 @@ TOOL="$ISABELLE_TOOL makeall $MFLAGS all" fi +IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT") + # main test loop log "starting [$@]" @@ -159,10 +163,16 @@ then # test log and cleanup echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 + if [ -x $PUBLISH_TEST ]; then + $PUBLISH_TEST -r $IDENT -s "SUCCESS" -a log $TESTLOG + fi gzip -f $TESTLOG else # test log echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 + if [ -x $PUBLISH_TEST ]; then + $PUBLISH_TEST -r $IDENT -s "FAIL" -a log $TESTLOG + fi # error log echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG