# HG changeset patch
# User krauss
# Date 1251981652 -7200
# Node ID eb82ed858b8481993a87ff1eb8b82136b353196d
# Parent  7a06bf89c038b6d2af95b89527606d7251b7ec08
isatest: collect test results and logs in testdata repository

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