diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-12 03:08:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 12:12:56 +0200 |
| commit | d53ba17d1761261593c598b6a88cfd6ce0eb3514 (patch) | |
| tree | df442236534c337d8eaba771ff15bebf4e806240 /lib/envars.ml | |
| parent | 34a2f9eb315da8b794f2573bdfc8ff941d81bdbe (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 'lib/envars.ml')
| -rw-r--r-- | lib/envars.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 989a18db9..b71a3f629 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,11 +110,8 @@ let guess_coqlib fail = let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in check_file_else ~dir ~file:prelude (fun () -> - let coqlib = match Coq_config.coqlib with - | Some coqlib -> coqlib - | None -> coqroot - in - if Sys.file_exists (coqlib / prelude) then coqlib + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) + then Coq_config.coqlib else fail "cannot guess a path for Coq libraries; please use -coqlib option") |