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 <theo.zimmi@gmail.com>
---
 ide/coqide.ml    | 2 --
 ide/coqide_ui.ml | 1 -
 2 files changed, 3 deletions(-)

(limited to 'ide')

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 918c196968..d7e155f6bb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -996,8 +996,6 @@ let build_ui () =
     item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
     item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
     item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
-    item "Revert all buffers" ~label:"_Revert all buffers"
-      ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED;
     item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE
       ~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer";
     item "Print..." ~label:"_Print..."
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index f056af6703..59dd9c0e4c 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -36,7 +36,6 @@ let init () =
 \n    <menuitem action='Save' />\
 \n    <menuitem action='Save as' />\
 \n    <menuitem action='Save all' />\
-\n    <menuitem action='Revert all buffers' />\
 \n    <menuitem action='Close buffer' />\
 \n    <menuitem action='Print...' />\
 \n    <menu action='Export to'>\
-- 
cgit v1.2.3