]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6150b8e) | patch
Bug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 May 2004 08:39:54 +0000 (08:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 May 2004 08:39:54 +0000 (08:39 +0000)
commit3fb7f6206485d474b576c38c0d622aea73e0f3f0
treed869c126e0bb86b6c8cb1e58405d3c2ba2a853adtree | snapshot
parent6150b8ef905aaea17b47ff466c067054f976cd8fcommit | diff
Bug fixed: the xml:base URL and helm:base URI were NOT base URL/URI: they
were full URIs (with also the filename at the end). Fixed by using
Filename.dirname (that seems to work also with generic URIs).
helm/ocaml/getter/http_getter_cache.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.