diff options
| -rw-r--r-- | ide/preferences.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index b7fdc975c2..b39a1106c2 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -924,8 +924,13 @@ let configure ?(apply=(fun () -> ())) () = vertical_tabs;opposite_tabs] in let edit_user_query (q, k) = - let q = Configwin_ihm.edit_string "User query" q in - let k = Configwin_ihm.edit_string "Shortcut key" k in + let input_string l s v = + match GToolbox.input_string ~title:l ~text:s v with + | None -> s + | Some s -> s + in + let q = input_string "User query" q "Your query" in + let k = input_string "Shortcut key" k "Shortcut (a single letter)" in q, k in |