diff: add a "Search in diff" feature
commitb43210b5a57f7449e158610488e0cd43eb071042
authorDavid Aguilar <davvid@gmail.com>
Mon, 13 Mar 2023 10:18:57 +0000 (13 03:18 -0700)
committerDavid Aguilar <davvid@gmail.com>
Mon, 13 Mar 2023 10:24:16 +0000 (13 03:24 -0700)
treee3ed92d96a187fe93eb31ee54401671b063d6d95
parentcf8d760066224fb9c198f1d19b8b24525b91ccbf
diff: add a "Search in diff" feature

Teach the diff editor to search within the diff text when the ctrl-f and
ctrl-g hotkeys are used.

Closes: #1116
Suggested-by: Giovanni Martins @GiovanniSM20 via github.com
Suggested-by: Dorian Marchal @dorian-marchal via github.com
Signed-off-by: David Aguilar <davvid@gmail.com>
CHANGES.rst
cola/hotkeys.py
cola/icons.py
cola/widgets/diff.py
cola/widgets/text.py
docs/hotkeys.html
docs/hotkeys_de.html
docs/hotkeys_zh_CN.html
docs/hotkeys_zh_TW.html