Admin/profiling_reports
author wenzelm
Tue Jul 10 16:45:05 2007 +0200 (2007-07-10)
changeset 23702 58ca991e0702
parent 23604 56f945f1ed50
child 24856 f06829479407
permissions -rwxr-xr-x
removed no_state markup -- produce empty state;
Markup.add_mode;
     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