Admin/profiling_reports
author wenzelm
Sun Jul 29 16:00:02 2007 +0200 (2007-07-29)
changeset 24053 af1dd276fae0
parent 23604 56f945f1ed50
child 24856 f06829479407
permissions -rwxr-xr-x
added ML toplevel use commands: Toplevel.program;
added install_pp stuff;
     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