commands renomme en queries, command goto a la place de forward to backwardt o

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5015 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/ide/preferences.mli b/ide/preferences.mli
index ba5d693e9..5cf26c90e 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -45,7 +45,9 @@ type pref =
       mutable contextual_menus_on_goal : bool;
       mutable window_width : int;
       mutable window_height : int;
+(*
       mutable use_utf8_notation : bool;
+*)
       mutable auto_complete : bool;
     }