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