equal
deleted
inserted
replaced
13 |
13 |
14 LOGDIR="$HOME/log" |
14 LOGDIR="$HOME/log" |
15 LOG="$LOGDIR/test-${DATE}-${HOST}.log" |
15 LOG="$LOGDIR/test-${DATE}-${HOST}.log" |
16 |
16 |
17 TEST_NAME="minimal-test" |
17 TEST_NAME="minimal-test" |
18 PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py" |
|
19 |
18 |
20 |
19 |
21 ## diagnostics |
20 ## diagnostics |
22 |
21 |
23 function fail() |
22 function fail() |
46 "$ISABELLE_TOOL" makeall all -k |
45 "$ISABELLE_TOOL" makeall all -k |
47 exit "$?" |
46 exit "$?" |
48 ) > "$LOG" 2>&1 |
47 ) > "$LOG" 2>&1 |
49 |
48 |
50 if [ "$?" -eq 0 ]; then |
49 if [ "$?" -eq 0 ]; then |
51 [ -x "$PUBLISH_TEST" ] && \ |
|
52 "$PUBLISH_TEST" -r "$IDENT" -s SUCCESS -a log "$LOG" -n "$TEST_NAME" |
|
53 gzip -f "$LOG" |
50 gzip -f "$LOG" |
54 else |
51 else |
55 [ -x "$PUBLISH_TEST" ] && \ |
|
56 "$PUBLISH_TEST" -r "$IDENT" -s FAIL -a log "$LOG" -n "$TEST_NAME" |
|
57 fail "Minimal test failed, see $LOG" |
52 fail "Minimal test failed, see $LOG" |
58 fi |
53 fi |
59 |
54 |