]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9620496) | patch
- added functions "add_server" and "remove_server" to dynamically adjust
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 13:33:42 +0000 (13:33 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 7 Apr 2003 13:33:42 +0000 (13:33 +0000)
commit4a44fbdb0e13c8d515f62d33e33e6b8cc519d74f
tree0c8f898d6f12cf300be99bbc4a25b93580e70230tree | snapshot
parent96204969d2611dc618f7ed72ae40612b9526c763commit | diff
- added functions "add_server" and "remove_server" to dynamically adjust
  servers list at runtime
helm/http_getter/http_getter_env.ml diff | blob | history
helm/http_getter/http_getter_env.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.