]> matita.cs.unibo.it Git - helm.git/commit
added "output" parameter to gzip and gunzip used to specify target file
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 12 Mar 2003 18:03:46 +0000 (18:03 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 12 Mar 2003 18:03:46 +0000 (18:03 +0000)
commit9e2208be9eaf40ff0d9c9c00d0a388bf930f7a27
tree7f3124a44f0025fcd8053caaf8c8f63eaaf88434
parentfbba267d392714a70c1eaa74fa6b2116ce1caadf
added "output" parameter to gzip and gunzip used to specify target file
for compression and decompression
helm/http_getter/http_getter_misc.ml
helm/http_getter/http_getter_misc.mli