I went through the code and looks good to me (note I'm not Colomban though ;-). In addition to the above patch, maybe two additional functionality-related notes:
- I think it would be good to filter also based on the group name - e.g. if I want all "git changebar" settings and type "git", all its children would be shown.
- I find it a bit strange that the filter text in the entry is preserved after closing and reopening the Preferences dialog. Wouldn't it be better to clear it?
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.
Message ID: <geany/geany/pull/4192/c2577379796@github.com>