Iris Morelle 38af14f1a8 gui2/preferences: Streamline filter options on the Hotkeys page
Categories vs. Filter both deal with filtering -- the only difference is
that categories has a broader scope than the name-based filtering, with
the latter being applied to results for the selected categories. We
don't need two rows for both.
2021-02-20 14:37:13 -03:00
..
2020-10-20 10:37:10 +02:00
2020-10-15 05:44:07 +02:00