]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b6856f3) | patch
catch CTRL-C and save maps before quitting
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Dec 2002 19:57:13 +0000 (19:57 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Dec 2002 19:57:13 +0000 (19:57 +0000)
commita96d06ae093236a3be8461912926903e81751578
tree0f2dc644838f812979de04012ee60556ffc9d0a5tree | snapshot
parentb6856f3de223e50ebeb3c26fd098ab128a5d661fcommit | diff
catch CTRL-C and save maps before quitting
helm/http_getter/http_getter.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.