Admin/profiling_reports
author wenzelm
Fri Oct 05 11:16:30 2007 +0200 (2007-10-05 ago)
changeset 24856 f06829479407
parent 23604 56f945f1ed50
child 36859 51af1657263b
permissions -rwxr-xr-x
cover only .gz files;
wenzelm@23604
     1
#!/usr/bin/env bash
wenzelm@23604
     2
#
wenzelm@23604
     3
# $Id$
wenzelm@23604
     4
# Author: Makarius
wenzelm@23604
     5
#
wenzelm@23604
     6
# DESCRIPTION: Cumulative reports for Poly/ML profiling output.
wenzelm@23604
     7
wenzelm@23604
     8
THIS=$(cd $(dirname "$0"); echo "$PWD")
wenzelm@23604
     9
wenzelm@23604
    10
SRC="$1"
wenzelm@23604
    11
DST="$2"
wenzelm@23604
    12
wenzelm@23604
    13
mkdir -p "$DST"
wenzelm@23604
    14
wenzelm@24856
    15
for FILE in "$SRC"/*.gz
wenzelm@23604
    16
do
wenzelm@23604
    17
  echo "$FILE"
wenzelm@23604
    18
  NAME="$(basename "$FILE" .gz)"
wenzelm@23604
    19
  gzip -dc "$FILE" | "$THIS/profiling_report" > "$DST/$NAME"
wenzelm@23604
    20
done