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:
1. 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. 2. 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 or view it on GitHub: https://github.com/geany/geany/pull/4192#issuecomment-2577379796 You are receiving this because you are subscribed to this thread. Message ID: <geany/geany/pull/4192/c2577379...@github.com>
