]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 641aec8) | patch
- added a destroy callback
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 4 Sep 2003 16:46:46 +0000 (16:46 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 4 Sep 2003 16:46:46 +0000 (16:46 +0000)
commit22bb9330d93cdf89baa5df76df6db72709a4d6fb
tree61d040441d986ef12e4a04ed5aa8c1414ad65c80tree | snapshot
parent641aec825f4cf10d5075da92681575acdfeeb2aecommit | diff
- added a destroy callback
- ignore delete events on hbugs window
- unsubscribe only when hbugs window gets _destroyed_
helm/hbugs/client/hbugs_client.ml diff | blob | history
helm/hbugs/client/hbugs_client.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.