From: Luca Padovani Date: Tue, 30 Jan 2001 09:18:06 +0000 (+0000) Subject: added support for compressed files X-Git-Tag: no-uwobo~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4e8b137b58ec6763785b8ee490ee8cd6cb77b5bf;p=helm.git added support for compressed files --- 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"; } }