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 /tools/coqdoc | |
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 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5d48473d8..4b5c5d2e5 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -74,19 +74,19 @@ let normalize_filename f = let guess_coqlib () = let file = "theories/Init/Prelude.vo" in - match Coq_config.coqlib with - | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib - | Some _ | None -> - let coqbin = normalize_path (Filename.dirname Sys.executable_name) in - let prefix = Filename.dirname coqbin in - let rpath = - if Coq_config.local then [] - else if Coq_config.arch_is_win32 then ["lib"] - else ["lib/coq"] - in - let coqlib = List.fold_left (/) prefix rpath in - if Sys.file_exists (coqlib / file) then coqlib - else prefix + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) + then Coq_config.coqlib + else + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let rpath = + if Coq_config.local then [] + else if Coq_config.arch_is_win32 then ["lib"] + else ["lib/coq"] + in + let coqlib = List.fold_left (/) prefix rpath in + if Sys.file_exists (coqlib / file) then coqlib + else prefix let header_trailer = ref true let header_file = ref "" |