From d5af8a969cfbd32484b4939bfeff153c86fc2fe2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Sep 2019 15:16:29 +0200
Subject: CoqIDE: removing option contextual menu on goal, inactive since
 2da5db43c.

---
 ide/preferences.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ide/preferences.mli')

diff --git a/ide/preferences.mli b/ide/preferences.mli
index 6da6228545..4b04326cec 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -79,7 +79,6 @@ val cmd_browse : string preference
 val cmd_editor : string preference
 val text_font : string preference
 val show_toolbar : bool preference
-val contextual_menus_on_goal : bool preference
 val window_width : int preference
 val window_height : int preference
 val auto_complete : bool preference
-- 
cgit v1.2.3