omit file extensions without any hits

This commit is contained in:
Joachim Reichel
2008-10-12 14:02:09 +00:00
parent 74408f73fe
commit 30282685d4
+6 -4
View File
@@ -98,10 +98,12 @@ echo
echo Detailed results excluding examples and demo:
for EXT in $EXTENSIONS; do
echo
echo $EXT files
echo
cat $PREFIX2.$EXT
if [ `cat $PREFIX2.$EXT | wc -l` -gt 0 ]; then
echo
echo $EXT files
echo
cat $PREFIX2.$EXT
fi
done
echo