]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd67635) | patch
- added handling of exceptions embedded in xml documents (usually coming
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)
commit9c313992f130290e8b8d97a7b199b9171784cecf
tree59b4558c736af0c2e6aabcb019f6a72a1cf95f4atree | snapshot
parentcd67635a6a717d848acf65789e612cc013d4fc1bcommit | diff
- added handling of exceptions embedded in xml documents (usually coming
  from http_getter)
- added exception Getter_failure which wraps the above exception
- added exception Parser_failure for generic errors
- removed useless EmptyUri exception
helm/ocaml/cic/cicParser.ml diff | blob | history
helm/ocaml/cic/cicParser.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.