--- 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