]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d8738e5) | patch
- added via_http parameter so that when the getter is used locally (i.e.
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 09:53:26 +0000 (09:53 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 6 Apr 2004 09:53:26 +0000 (09:53 +0000)
commitf44ab01307f10d4165c76e3108542a5bc2035766
treeffd0f69e62a179b841aa69060aed7837ffc06749tree | snapshot
parentd8738e52af861cbdda5268671b30183b99d51c54commit | diff
- added via_http parameter so that when the getter is used locally (i.e.
  as a library), http specific messages aren't generated
- use polymorphic variants for some configuration parameters
- better logging on /update (<br> tags are now generated)
helm/ocaml/getter/http_getter.ml diff | blob | history
helm/ocaml/getter/http_getter_cache.ml diff | blob | history
helm/ocaml/getter/http_getter_cache.mli diff | blob | history
helm/ocaml/getter/http_getter_common.ml diff | blob | history
helm/ocaml/getter/http_getter_common.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.