]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cdef799) | patch
- added some default values (no longer explicitely required in the
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 14:02:20 +0000 (14:02 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 4 Feb 2005 14:02:20 +0000 (14:02 +0000)
commit0167f31845a56f4e1eda4035299d878b203fc633
tree1c986fb9e3b87278ec5529653bf487cec04f5260tree | snapshot
parentcdef799a0e2e3c7db8bb2b95cd124767a4126c61commit | diff
- added some default values (no longer explicitely required in the
  configuration file)
- bugfix: read configuration values from the environment and not
  directly via Helm_registry
helm/http_getter/main.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.