diff options
Diffstat (limited to 'doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst')
| -rw-r--r-- | doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst deleted file mode 100644 index 9d22a858f1..0000000000 --- a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - "Revert all buffers" command from CoqIDE which had been broken for a long time - (`#11415 <https://github.com/coq/coq/pull/11415>`_, - by Pierre-Marie Pédrot). |