--- a/Admin/isatest/minimal-test Mon Jul 30 15:54:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: minimal test of current repository version
-
-## global settings
-
-MAXTIME=14400
-
-DATE=$(date "+%Y-%m-%d_%H:%M")
-HOST=$(hostname -s)
-
-LOGDIR="$HOME/log"
-LOG="$LOGDIR/test-${DATE}-${HOST}.log"
-
-TEST_NAME="minimal-test"
-
-
-## diagnostics
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-mkdir -p "$LOGDIR" || fail "Bad log directory: $LOGDIR"
-
-[ -z "$ISABELLE_HOME" -o -z "$ISABELLE_TOOL" ] && fail "Bad Isabelle environment"
-
-cd "$ISABELLE_HOME"
-
-hg pull -u || fail "Bad repository: $PWD"
-IDENT="$(hg parent --template "{node|short}")"
-
-(
- ulimit -t "$MAXTIME"
-
- echo -n "hg id: "; hg id
- "$ISABELLE_TOOL" makeall clean
- "$ISABELLE_TOOL" makeall all -k
- exit "$?"
-) > "$LOG" 2>&1
-
-if [ "$?" -eq 0 ]; then
- gzip -f "$LOG"
-else
- fail "Minimal test failed, see $LOG"
-fi
-