diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/util.ml | 5 | ||||
| -rw-r--r-- | src/util.mli | 2 |
2 files changed, 7 insertions, 0 deletions
diff --git a/src/util.ml b/src/util.ml index b45f011..2bac3d6 100644 --- a/src/util.ml +++ b/src/util.ml @@ -20,3 +20,8 @@ let string_of_path path = match path with | [] -> "" | x :: xs -> Printf.sprintf "%s%s" x (aux xs "") + +let substitute_default o d = + match o with + | None -> d + | Some v -> v diff --git a/src/util.mli b/src/util.mli index ec0bb73..7d78a15 100644 --- a/src/util.mli +++ b/src/util.mli @@ -1,3 +1,5 @@ val find_xml_child : string -> Xml.xml -> Xml.xml option val string_of_path : string list -> string + +val substitute_default : 'a option -> 'a -> 'a |