# HG changeset patch
# User wenzelm
# Date 1191575790 -7200
# Node ID f06829479407e2abd5d6af7e37719bc495855c0a
# Parent  161eb8381b4940bb00a174cccf840e86c25cd405
cover only .gz files;

diff -r 161eb8381b49 -r f06829479407 Admin/profiling_reports
--- a/Admin/profiling_reports	Fri Oct 05 09:59:21 2007 +0200
+++ b/Admin/profiling_reports	Fri Oct 05 11:16:30 2007 +0200
@@ -12,7 +12,7 @@
 
 mkdir -p "$DST"
 
-for FILE in "$SRC"/*
+for FILE in "$SRC"/*.gz
 do
   echo "$FILE"
   NAME="$(basename "$FILE" .gz)"