Admin/profiling_reports
author wenzelm
Thu Nov 26 15:28:42 2009 +0100 (2009-11-26)
changeset 33905 5760ba045bf0
parent 24856 f06829479407
child 36859 51af1657263b
permissions -rwxr-xr-x
additional menu entries;
     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"/*.gz
    16 do
    17   echo "$FILE"
    18   NAME="$(basename "$FILE" .gz)"
    19   gzip -dc "$FILE" | "$THIS/profiling_report" > "$DST/$NAME"
    20 done