aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index e1e524cf4a..b96eca3ae3 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -65,6 +65,8 @@ let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
(* Lists *)
+let list_add_set x l = if List.mem x l then l else x::l
+
let list_intersect l1 l2 =
List.filter (fun x -> List.mem x l2) l1