aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/envars.mli b/lib/envars.mli
index fbcbfe72af..e99fd8e03e 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -26,5 +26,6 @@ val xdg_dirs : warn:(string -> unit) -> string list
val coqpath : string list
val camlbin : unit -> string
+val camlp4bin : unit -> string
val camllib : unit -> string
val camlp4lib : unit -> string