summaryrefslogtreecommitdiff
path: root/src/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/util.ml')
-rw-r--r--src/util.ml5
1 files changed, 5 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