Admin/isatest/minimal-test
changeset 48212 cccc92c0addc
parent 33859 033ce4cafba6
--- 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