cover only .gz files;
authorwenzelm
Fri Oct 05 11:16:30 2007 +0200 (2007-10-05)
changeset 24856f06829479407
parent 24855 161eb8381b49
child 24857 2dde4189a055
cover only .gz files;
Admin/profiling_reports
     1.1 --- a/Admin/profiling_reports	Fri Oct 05 09:59:21 2007 +0200
     1.2 +++ b/Admin/profiling_reports	Fri Oct 05 11:16:30 2007 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  mkdir -p "$DST"
     1.6  
     1.7 -for FILE in "$SRC"/*
     1.8 +for FILE in "$SRC"/*.gz
     1.9  do
    1.10    echo "$FILE"
    1.11    NAME="$(basename "$FILE" .gz)"