]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ae25bae) | patch
- better handling of temp files wrt to failures. When a temp file has
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Feb 2004 16:14:58 +0000 (16:14 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Feb 2004 16:14:58 +0000 (16:14 +0000)
commitc19ffb699f8f4681f0c7d9f59fae96f2023cd058
tree41f7ec00f351f2dc2a00902c529ab1e6fe3410aatree | snapshot
parentae25bae855f66b7ebc9926a80dc38e622f0cff38commit | diff
- better handling of temp files wrt to failures. When a temp file has
  been created and an exception is raised, the exception will be
  catched, the tempfile deleted and the exception raised again
helm/ocaml/getter/http_getter_cache.ml diff | blob | history
helm/ocaml/getter/http_getter_cache.mli diff | blob | history
helm/ocaml/getter/http_getter_common.ml diff | blob | history
helm/ocaml/getter/http_getter_types.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.