From 4e8b137b58ec6763785b8ee490ee8cd6cb77b5bf Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Tue, 30 Jan 2001 09:18:06 +0000 Subject: [PATCH] added support for compressed files --- helm/interface/uris_of_filenames.pl | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/interface/uris_of_filenames.pl b/helm/interface/uris_of_filenames.pl index e06ac822a..019730bee 100755 --- a/helm/interface/uris_of_filenames.pl +++ b/helm/interface/uris_of_filenames.pl @@ -4,12 +4,14 @@ while() { chomp; split / /; for (@_) { + $GZSUFF = ""; + if (/.gz$/) + { s/.gz$//; $GZSUFF = " gz" if ($ARGV[0] == "-gz"); } if (/.*\.(con|var|ind)(\.types)?\.xml/) { s/\./cic:/; } elsif (/.*\.theory\.xml/) { s/\./theory:/; } s/\.xml//; - print; - print "\n"; + print $_.$GZSUFF."\n"; } } -- 2.39.2