diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-14 14:04:12 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-14 14:07:20 +0100 |
| commit | fa08993b9330623c8cb259ac8ebff93ecce9c2f6 (patch) | |
| tree | a96caf2878485a3ba0cf39d6e1c9d6896deee6a4 /ide/preferences.ml | |
| parent | 317858b7ad05764a2ce010354631443f219a4b9f (diff) | |
CoqIDE: add 'you need to restart CoqIDE after changing shortcuts' message
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 01ce45483..8988dbc60 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -754,6 +754,13 @@ let configure ?(apply=(fun () -> ())) () = "Allowed modifiers" the_valid_mod in + let modifier_notice = + let b = GPack.hbox () in + let _lbl = + GMisc.label ~markup:"You need to <b>restart CoqIDE</b> after changing these settings" + ~packing:b#add () in + custom b (fun () -> ()) true + in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo @@ -855,7 +862,7 @@ 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; modifier_notice]); Section("Misc", Some `ADD, misc)] in |