--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-stats	Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,51 @@
+#!/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