diff options
| -rw-r--r-- | lib/gmapl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/gmapl.ml b/lib/gmapl.ml index 17c6c4b3ea..8fc2daf96a 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -21,7 +21,7 @@ let fold = Gmap.fold let add x y m = try let l = Gmap.find x m in - Gmap.add x (if List.mem y l then l else y::l) m + Gmap.add x (y::list_except y l) m with Not_found -> Gmap.add x [y] m |