Javi Merino 754d074027 Add an option to remove event numbers from search ...

Event numbers don't add information to the search: if you knew the
event number you wouldn't be searching for the command.  Add an option
to remove them from the search to declutter it.  Default it to true to
preserve the current behaviour.

2022-05-09 07:21:59 +01:00

1.5 KiB

Raw Blame History

View Raw