diff options
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r-- | ide/preferences.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 9fe9c6337..44a89edf9 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -643,6 +643,10 @@ let pmodifiers ?(all = false) name p = modifiers name (str_to_mod_list p#get) +[@@@ocaml.warning "-3"] (* String.uppercase_ascii since 4.03.0 GPR#124 *) +let uppercase = String.uppercase +[@@@ocaml.warning "+3"] + let configure ?(apply=(fun () -> ())) () = let cmd_coqtop = string @@ -969,7 +973,7 @@ let configure ?(apply=(fun () -> ())) () = let k = if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k else "" in - let k = CString.uppercase k in + let k = uppercase k in [q, k] in |