diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-11 11:11:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 11:21:21 +0200 |
| commit | 417ac448411ce924444915da8e7e6fb81a12bc57 (patch) | |
| tree | f9ab75068617f0c0a598e058da206803883d0103 /config | |
| parent | 168bb8fd5fe62beebd5e4998e903777b33654a4a (diff) | |
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.
Diffstat (limited to 'config')
| -rw-r--r-- | config/coq_config.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index c171bd355..59c96f73d 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 *) |