aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/nanoPG.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2013-12-03 09:55:04 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2013-12-03 09:55:04 +0100
commit1e5e934a8ce31c129368e57b61e485e6b989c3f4 (patch)
tree5ea4ce12c4faf03b631f452e4a362eb40bc422b5 /ide/nanoPG.ml
parent24d17c1084d0926047b7ce5c7e3adac43f62378a (diff)
Silence compilation warning by avoiding some deprecated constructs.
Diffstat (limited to 'ide/nanoPG.ml')
-rw-r--r--ide/nanoPG.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml
index dafb0575d..fe9e815c9 100644
--- a/ide/nanoPG.ml
+++ b/ide/nanoPG.ml
@@ -64,7 +64,7 @@ let make_emacs_mode gui name enter_sym bindings =
let compile_emacs_modes gui l =
List.fold_left (fun (r,s,u,m,d) mode ->
let run, set, unset, mask,doc = mode gui in
- (fun k -> r k || run k), (fun k -> s k or set k),
+ (fun k -> r k || run k), (fun k -> s k || set k),
(fun () -> u (); unset ()), (fun k -> m k || mask k), d^"\n"^doc)
((fun _ -> false),(fun _ -> false),(fun () -> ()),(fun _ -> false),"") l