Admin/isatest-stats

tuned;

#!/usr/bin/env bash
#
# $Id$
# Author: Makarius
#
# DESCRIPTION: Standard statistics.

THIS=$(cd "$(dirname "$0")"; pwd -P)

for PLATFORM in at-poly at-sml-dev
do
  "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 1000 \
    HOL \
    HOL-Algebra \
    HOL-Auth \
    HOL-Bali \
    HOL-Complex \
    HOL-Extraction \
    HOL-Hoare \
    HOL-HoareParallel \
    HOL-Lambda \
    HOL-MicroJava \
    HOL-NumberTheory \
    HOL-SET-Protocol \
    HOL-UNITY \
    HOL-ex \
    ZF \
    ZF-Constructible
done