aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-12 04:01:29 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-29 12:12:57 +0200
commit5c875b6ab907cb48b0d06aba48d4c733cfd2ff06 (patch)
treeaec2a11ab2b73620eb02b49c412f645f7241f868 /lib/envars.mli
parent66b98ecd41bac232bbee19a9b3484feefd71df3c (diff)
Relying on computation done in Envars to discover the installation directories.
This allows to share the test for possible relocalisation done in envars.ml.
Diffstat (limited to 'lib/envars.mli')
-rw-r--r--lib/envars.mli12
1 files changed, 9 insertions, 3 deletions
diff --git a/lib/envars.mli b/lib/envars.mli
index c33a08c40..c8bbf17d9 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -27,12 +27,18 @@ val home : warn:(string -> unit) -> string
(** [coqlib] is the path to the Coq library. *)
val coqlib : unit -> string
+(** [docdir] is the path to the installed documentation. *)
+val docdir : unit -> string
+
+(** [datadir] is the path to the installed data directory. *)
+val datadir : unit -> string
+
+(** [configdir] is the path to the installed config directory. *)
+val configdir : unit -> string
+
(** [set_coqlib] must be runned once before any access to [coqlib] *)
val set_coqlib : fail:(string -> string) -> unit
-(** [docdir] is the path to the Coq documentation. *)
-val docdir : unit -> string
-
(** [coqbin] is the name of the current executable. *)
val coqbin : string