# HG changeset patch
# User wenzelm
# Date 1343657005 -7200
# Node ID e24bfa4e3b84436b704ce624feeccbbffb3d2c4b
# Parent  4b6c90e121b1936169c1de1cc082fe781adc120d
obsolete;

diff -r 4b6c90e121b1 -r e24bfa4e3b84 Admin/isatest/minimal-test
--- 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
-