diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest-stats --- 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" < - -Development Snapshot -- Performance Statistics - - -

$PLATFORM

-EOF - -for SESSION in $SESSIONS -do - echo "

" >> "stats/$PLATFORM.html" -done - -echo "" >> "stats/$PLATFORM.html" -echo "" >> "stats/$PLATFORM.html" - -done