# HG changeset patch
# User wenzelm
# Date 1183715705 -7200
# Node ID 56f945f1ed50bfd8270e3aadb9e2d8ec280e0d0e
# Parent  4a2e364753676ca97c0260a7484c62f4be57a4ba
Cumulative reports for Poly/ML profiling output.

diff -r 4a2e36475367 -r 56f945f1ed50 Admin/profiling_reports
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/profiling_reports	Fri Jul 06 11:55:05 2007 +0200
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Makarius
+#
+# DESCRIPTION: Cumulative reports for Poly/ML profiling output.
+
+THIS=$(cd $(dirname "$0"); echo "$PWD")
+
+SRC="$1"
+DST="$2"
+
+mkdir -p "$DST"
+
+for FILE in "$SRC"/*
+do
+  echo "$FILE"
+  NAME="$(basename "$FILE" .gz)"
+  gzip -dc "$FILE" | "$THIS/profiling_report" > "$DST/$NAME"
+done