]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 73ad098) | patch
- simplified environment handling:
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 09:26:59 +0000 (09:26 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 09:26:59 +0000 (09:26 +0000)
commit912cf238365dbf70aed65c5a0bc65e5f3c1ea92b
treeb799eb5ed4b1655ef539145ae58061df05bda9a3tree | snapshot
parent73ad0985990447db97f17870d2744f8fda13ebe4commit | diff
- simplified environment handling:
  * added a lot of default values
  * use maps_dir instead of dbm files file-per-file
  * use cache_dir instead of cache dirs dir-per-dir
  * servers could now either be listed in servers.txt or directly in
    configuration file
helm/ocaml/getter/http_getter_env.ml diff | blob | history
helm/ocaml/getter/http_getter_env.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.