From f38dea0dd11f87c5e7cf1db5c8ed1168dd672974 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jan 2020 12:59:19 +0100 Subject: Remove the CoqIDE "Revert all Buffers" command. Fixes #3907: CoqIDE File->Revert all buffers does not work. Co-Authored-By: Théo Zimmermann --- doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst (limited to 'doc') 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 new file mode 100644 index 0000000000..cb92945b8b --- /dev/null +++ b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Revert all buffers" command from CoqIDE which had been broken for a long time + (`#11415 `_, + by Pierre-Marie Pédrot). -- cgit v1.2.3