diff options
| author | Hugo Herbelin | 2019-09-10 15:16:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-10 15:20:58 +0200 |
| commit | d5af8a969cfbd32484b4939bfeff153c86fc2fe2 (patch) | |
| tree | ca2b5d078342e7ea0cef220e7700e2b4cc228fc3 /ide/preferences.mli | |
| parent | f612bee8c1723b4d66fe1ba93dbb23f5bd201ae6 (diff) | |
CoqIDE: removing option contextual menu on goal, inactive since 2da5db43c.
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 1 |
1 files changed, 0 insertions, 1 deletions
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 |