From 417ac448411ce924444915da8e7e6fb81a12bc57 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Nov 2016 11:11:20 +0100
Subject: Configuration: always giving a value to configdir and datadir.

They were not used for looking for coqide files in the situation when
the effective installation path happens to be exactly the installation
path proposed by default, while relevant files were however (possibly)
installed in these directories.
---
 config/coq_config.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'config')

diff --git a/config/coq_config.mli b/config/coq_config.mli
index c171bd3553..59c96f73d0 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -9,8 +9,8 @@
 val local : bool        (* local use (no installation) *)
 
 val coqlib : string option (* where the std library is installed *)
-val configdir : string option (* where configuration files are installed *)
-val datadir : string option (* where extra data files are 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 *)
 
 val ocaml : string      (* names of ocaml binaries *)
-- 
cgit v1.2.3


From d53ba17d1761261593c598b6a88cfd6ce0eb3514 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Nov 2016 03:08:56 +0100
Subject: 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.
---
 config/coq_config.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'config')

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 59c96f73d0..28a40ca938 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 *)
-- 
cgit v1.2.3


From 58935ddbaf6f0e2470716d30f70ea18a9f8151c4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Nov 2016 03:08:34 +0100
Subject: Exporting the suffixes needed to build coqlib, docdir, etc.

This allows to centralize in the configuration file the description of
the 3 possible installation layouts (dispatched over directories
shared by multiple application as in unix, self-contained style like
in windows, local non-installation as with option -local).

Also supporting relocalisation when -prefix or -libdir and co is given.
---
 config/coq_config.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'config')

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 28a40ca938..2b3bc2c25b 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -8,11 +8,19 @@
 
 val local : bool        (* local use (no installation) *)
 
+(* The fields below are absolute paths *)
 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 *)
 
+(* The fields below are paths relative to the installation prefix *)
+(* However, if an absolute path, it means discarding the actual prefix *)
+val coqlibsuffix : string    (* std library relative to installation prefix *)
+val configdirsuffix : string (* config files relative to installation prefix *)
+val datadirsuffix : string   (* data files relative to installation prefix *)
+val docdirsuffix : string    (* doc directory relative to installation prefix *)
+
 val ocaml : string      (* names of ocaml binaries *)
 val ocamlfind : string
 val ocamllex : string
-- 
cgit v1.2.3