aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-12 03:08:56 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-29 12:12:56 +0200
commitd53ba17d1761261593c598b6a88cfd6ce0eb3514 (patch)
treedf442236534c337d8eaba771ff15bebf4e806240 /config
parent34a2f9eb315da8b794f2573bdfc8ff941d81bdbe (diff)
Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.
This goes towards an approach where a local layout can be seen as an installed layout.
Diffstat (limited to 'config')
-rw-r--r--config/coq_config.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 59c96f73d..28a40ca93 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -8,7 +8,7 @@
val local : bool (* local use (no installation) *)
-val coqlib : string option (* where the std library is installed *)
+val coqlib : string (* where the std library is installed *)
val configdir : string (* where configuration files are installed *)
val datadir : string (* where extra data files are installed *)
val docdir : string (* where the doc is installed *)