]> matita.cs.unibo.it Git - helm.git/commit - helm/ocaml/getter/http_getter_map.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0a89d7d) | patch
The normalization of URIs when the DB is empty (or it is being filled) is
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 9 Jun 2004 13:12:23 +0000 (13:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 9 Jun 2004 13:12:23 +0000 (13:12 +0000)
commit3289eda62f4b44bc5043abd2acff602f7a8e5f26
treec64feccf2693e24b798ace45c3d317ea4c2d47cdtree | snapshot
parent0a89d7d0dbd950aa7f0248c30f16b7c2b1053cd7commit | diff
The normalization of URIs when the DB is empty (or it is being filled) is
not reliable. As a consequence the semantics of the Http_getter_map has been
changed again: the only method that normalized the URIs before using them
is the resolve method. The methods replace, add, remove, etc. no longer
normalize their argument.
helm/ocaml/getter/http_getter_map.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.