Hotkeys work just fine with me, the toggle on/off. Is it '$number'. 1. That would make the filter harder to implement - I just went with the easy option.
2. The flag on the bottom is not the currently selected category, but the category of the current message. Maybe the tooltip should be clearer - "Type of this message: " maybe? -- https://code.launchpad.net/~widelands-dev/widelands/bug-987510/+merge/236231 Your team Widelands Developers is requested to review the proposed merge of lp:~widelands-dev/widelands/bug-987510 into lp:widelands. _______________________________________________ Mailing list: https://launchpad.net/~widelands-dev Post to : widelands-dev@lists.launchpad.net Unsubscribe : https://launchpad.net/~widelands-dev More help : https://help.launchpad.net/ListHelp
