From abd469790c2e144f693e1b21c5cdc03aee178e6d Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 11:34:10 +0200 Subject: Merge the user queries tab with the shortcut tab. --- ide/preferences.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'ide/preferences.ml') diff --git a/ide/preferences.ml b/ide/preferences.ml index b39a1106c..6bb19c638 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -976,11 +976,10 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation]); + modifier_for_templates; modifier_for_display; modifier_for_navigation; + user_queries]); Section("Misc", Some `ADD, - misc); - Section("User queries", None, - [user_queries])] + misc)] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); -- cgit v1.2.3