aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorslrnsc2021-02-01 01:05:47 +0000
committerGitHub2021-02-01 01:05:47 +0000
commit36b07c2194466ed79977d0195cd6567dd2059d3b (patch)
tree7f394014f78a6a79634a26263e91be33ef600ddb
parent5ee09a9ed5d0ce7508ce63b77e04879995beb33f (diff)
Add changelog entry
-rw-r--r--doc/changelog/09-coqide/13810-shift-return-search-backwards.rst3
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst
new file mode 100644
index 0000000000..e78280d91d
--- /dev/null
+++ b/doc/changelog/09-coqide/13810-shift-return-search-backwards.rst
@@ -0,0 +1,3 @@
+- **Added:**
+ Shift-return in the Find dialog now searches backwards (`#13810 <https://github.com/coq/coq/pull/13810>`_,
+ by slrnsc).