Re: Widget not destroyed (webkit-gtk bindings)
Adrien <[email protected]> Fri, 23 Jan 2009 11:45:29 +0100
| Newsgroups | gmane.comp.lang.ocaml.lib.gtk |
|---|---|
| Message-ID | <[email protected]> |
Hi, I finally found the problem. I am now using Gc.full_major as Jacques Garrigues mentionned in an earlier answer. I had tried using it but had forgotten a reference to the view. I also had the following not-so-surprising problem which I failed to notice : in the following function, Gc.full_major will not finalize the view. let kill_view record_with_view_in_it = record_with_view_in_it.view#destroy; record_with_view_in_it.view <- Obj.magic 0; Gc.full_major () So I now call Gc.full_major in another function. --- Adrien Nader