# HG changeset patch
# User krauss
# Date 1341860920 -7200
# Node ID cccc92c0addc01cbfcadd0443081cc4dafc3e901
# Parent  12bbb9d4b6ede0d775b7dbef139b243503ef8638
abandoned import of isatest reports into (old version of) mira -- unstable, and not worth the maintenance effort

diff -r 12bbb9d4b6ed -r cccc92c0addc Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Mon Jul 09 09:28:26 2012 +1000
+++ b/Admin/isatest/isatest-makeall	Mon Jul 09 21:08:40 2012 +0200
@@ -10,8 +10,6 @@
 # max time until test is aborted (in sec)
 MAXTIME=28800
 
-PUBLISH_TEST="$HOME/home/isabelle-repository/repos/testtool/publish_test.py"
-
 ## diagnostics
 
 PRG="$(basename "$0")"
@@ -178,16 +176,10 @@
     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 -n Makeall_isatest_$SHORT
-        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 -n Makeall_isatest_$SHORT
-        fi
 
         # error log
         echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
diff -r 12bbb9d4b6ed -r cccc92c0addc Admin/isatest/minimal-test
--- a/Admin/isatest/minimal-test	Mon Jul 09 09:28:26 2012 +1000
+++ b/Admin/isatest/minimal-test	Mon Jul 09 21:08:40 2012 +0200
@@ -15,7 +15,6 @@
 LOG="$LOGDIR/test-${DATE}-${HOST}.log"
 
 TEST_NAME="minimal-test"
-PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py"
 
 
 ## diagnostics
@@ -48,12 +47,8 @@
 ) > "$LOG" 2>&1
 
 if [ "$?" -eq 0 ]; then
-  [ -x "$PUBLISH_TEST" ] && \
-    "$PUBLISH_TEST" -r "$IDENT" -s SUCCESS -a log "$LOG" -n "$TEST_NAME"
   gzip -f "$LOG"
 else
-  [ -x "$PUBLISH_TEST" ] && \
-    "$PUBLISH_TEST" -r "$IDENT" -s FAIL -a log "$LOG" -n "$TEST_NAME"
   fail "Minimal test failed, see $LOG"
 fi