abandoned import of isatest reports into (old version of) mira -- unstable, and not worth the maintenance effort
--- 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
--- 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