--- a/Admin/isatest-stats Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Makarius
-#
-# DESCRIPTION: Standard statistics.
-
-THIS=$(cd "$(dirname "$0")"; pwd -P)
-
-PLATFORMS="at-poly at-sml-dev at-mac-poly-e at64-poly-e"
-SESSIONS="\
- HOL \
- HOL-Algebra \
- HOL-Auth \
- HOL-Bali \
- HOL-Complex \
- HOL-Complex-ex \
- HOL-Extraction \
- HOL-Hoare \
- HOL-HoareParallel \
- HOL-Lambda \
- HOL-MicroJava \
- HOL-NumberTheory \
- HOL-SET-Protocol \
- HOL-UNITY \
- HOL-ex \
- ZF \
- ZF-Constructible\
- ZF-UNITY"
-
-for PLATFORM in $PLATFORMS
-do
- "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
- cat > "stats/$PLATFORM.html" <<EOF
-<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-<head><title>Development Snapshot -- Performance Statistics</title></head>
-
-<body>
-<h1>$PLATFORM</h1>
-EOF
-
-for SESSION in $SESSIONS
-do
- echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
-done
-
-echo "</body>" >> "stats/$PLATFORM.html"
-echo "</html>" >> "stats/$PLATFORM.html"
-
-done