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