diff options
| author | Gaëtan Gilbert | 2019-07-09 12:50:27 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-09 12:50:27 +0200 |
| commit | 35d8ca72adcc3ce04cb2919c4a2d60ea0c73d24c (patch) | |
| tree | cd44fa1b1b9e70f73b19d0616499b63016419db9 /ide | |
| parent | 7f366a7c7cd154c6a1dd191ff7f453e63b39a948 (diff) | |
| parent | dda7d129dba6c90d642cd99cd989e5f13c0eb4b4 (diff) | |
Merge PR #10471: [core] [api] Support OCaml 4.08
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/protocol/richpp.ml | 6 | ||||
| -rw-r--r-- | ide/session.ml | 4 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml index 507b985d2f..463d93af0d 100644 --- a/ide/protocol/richpp.ml +++ b/ide/protocol/richpp.ml @@ -94,7 +94,7 @@ let rich_pp width ppcmds = print_close_tag = ignore; } in - pp_set_formatter_tag_functions ft tag_functions; + pp_set_formatter_tag_functions ft tag_functions [@warning "-3"]; pp_set_mark_tags ft true; (* Setting the formatter *) @@ -107,9 +107,9 @@ let rich_pp width ppcmds = (* The whole output must be a valid document. To that end, we nest the document inside <pp> tags. *) pp_open_box ft 0; - pp_open_tag ft "pp"; + pp_open_tag ft "pp" [@warning "-3"]; Pp.(pp_with ft ppcmds); - pp_close_tag ft (); + pp_close_tag ft () [@warning "-3"]; pp_close_box ft (); (* Get the resulting XML tree. *) diff --git a/ide/session.ml b/ide/session.ml index 3792730455..a9c106a765 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -275,9 +275,9 @@ let make_table_widget ?sort cd cb = let make_sorting i (_, c) = let sort (store : GTree.model) it1 it2 = match c with | `IntC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) | `StringC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) in store#set_sort_func i sort in diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7758d89ed8..98390e810f 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -15,7 +15,7 @@ struct (* we use first size, then usual comparison *) let d = String.length s1 - String.length s2 in if d <> 0 then d - else Pervasives.compare s1 s2 + else compare s1 s2 end module Proposals = Set.Make(StringOrd) |