# HG changeset patch # User wenzelm # Date 1158699712 -7200 # Node ID 3f763be47c2f5a0ed29fce1f9d317970aec13d3f # Parent ca59894f70dca9f845384efb57c514782fd990ba simple html output; diff -r ca59894f70dc -r 3f763be47c2f Admin/isatest-stats --- a/Admin/isatest-stats Tue Sep 19 22:04:38 2006 +0200 +++ b/Admin/isatest-stats Tue Sep 19 23:01:52 2006 +0200 @@ -7,23 +7,43 @@ THIS=$(cd "$(dirname "$0")"; pwd -P) -for PLATFORM in at-poly at-sml-dev +PLATFORMS="at-poly at-sml-dev" +SESSIONS="\ + 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" + +for PLATFORM in $PLATFORMS do - "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 \ - 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 + "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" 100 $SESSIONS + cat > "stats/$PLATFORM.html" < + + Development Snapshot -- Statistics + + +

$PLATFORM

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

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