Work around WebKit bug 119003 by flushing events when removing a page from a window.

See <https://bugs.webkit.org/show_bug.cgi?id=119003>

git-svn-id: svn+ssh://svn.gnucash.org/repo/gnucash/trunk@23440 57a11ea4-9604-0410-9ed3-97b8803252fd
This commit is contained in:
Mike Alexander 2013-11-26 05:36:49 +00:00
parent da89f13f23
commit 5cff297872

View File

@ -2787,6 +2787,12 @@ gnc_main_window_disconnect (GncMainWindow *window,
{
page_num = gtk_notebook_page_num(notebook, new_page->notebook_page);
gtk_notebook_set_current_page(notebook, page_num);
/* This may have caused WebKit to schedule a timer interrupt which it
sometimes forgets to cancel before deleting the object. See
<https://bugs.webkit.org/show_bug.cgi?id=119003>. Get around this
by flushing all events to get rid of the timer interrupt. */
while (gtk_events_pending())
gtk_main_iteration();
}
}