Admin/isatest-stats
changeset 20615 0d71cc267e0d
parent 20613 8f2731bfe86f
child 20617 ca59894f70dc
--- a/Admin/isatest-stats	Tue Sep 19 21:49:38 2006 +0200
+++ b/Admin/isatest-stats	Tue Sep 19 22:00:32 2006 +0200
@@ -7,20 +7,23 @@
 
 THIS=$(cd "$(dirname "$0")"; pwd -P)
 
-"$THIS/isatest-statistics" stats/at-poly at-poly 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
+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