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