![]() There appears to be no way to make `on-demand' work right for the Unity window manager's global menu bar, since there's no notificiation when the menu bar is clicked. We approximate the correct behavior by calling `on-demand' when a containing frame loses the keyboard focus, which might be because the menu bar was clicked; that may be too late (because the menu has already been shown), but it should work most of the time. Closes PR 13347. Relevant to PR 13395, but DrRacket will have to change to work around the remaining limitations of `on-demand'. original commit: 55f98a15d4728ff843f2e5cdb5deef96b24da27b |
||
---|---|---|
.. | ||
framework | ||
gui |