]> matita.cs.unibo.it Git - helm.git/commit
- changes defaults of getxml (format gzipped, don't patch dtd)
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 10 May 2005 10:59:13 +0000 (10:59 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 10 May 2005 10:59:13 +0000 (10:59 +0000)
commit52fdcda3e0083391fa04a064f3e07279d975d5ba
treed197f92203111b6f5324d010458ea19b24ab8fdd
parentf693e2de79c1a95422a5efd22acbcea5003eeaba
- changes defaults of getxml (format gzipped, don't patch dtd)
- big bug fix which avoid spurious \n at end of gzipped file
helm/ocaml/getter/Makefile
helm/ocaml/getter/http_getter.ml
helm/ocaml/getter/http_getter.mli
helm/ocaml/getter/http_getter_cache.ml
helm/ocaml/getter/http_getter_common.ml
helm/ocaml/getter/http_getter_common.mli
helm/ocaml/getter/http_getter_misc.ml
helm/ocaml/getter/http_getter_misc.mli