summaryrefslogtreecommitdiff
path: root/src/options.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/options.mli')
-rw-r--r--src/options.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/options.mli b/src/options.mli
new file mode 100644
index 0000000..64bee51
--- /dev/null
+++ b/src/options.mli
@@ -0,0 +1,4 @@
1type t
2val default : t
3val with_height : int -> t -> t
4val with_marker : Marker.t -> t -> t