]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/papers/use_case/stats/stats_candidates_c1.sh
* basic infrastructure for collecting statistics
[helm.git] / helm / papers / use_case / stats / stats_candidates_c1.sh
diff --git a/helm/papers/use_case/stats/stats_candidates_c1.sh b/helm/papers/use_case/stats/stats_candidates_c1.sh
new file mode 100755 (executable)
index 0000000..3dee0a1
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/sh
+DEST=stats_candidates_c1
+DESTXML=$DEST.xml
+echo "<statistics>" >$DESTXML
+for i in `fgrep -v '#' CANDIDATI`; do
+  SOURCE=`echo $i | tr ":/'" '_' `.gz
+  ./stats.sh CONTENTNB/$SOURCE >>$DESTXML
+done
+echo "</statistics>" >>$DESTXML
+gzip $DESTXML