diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /tools/coqdoc/cdglobals.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'tools/coqdoc/cdglobals.ml')
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5d48473d..0d3fb775 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -70,23 +72,21 @@ let normalize_filename f = let dirname = Filename.dirname f in normalize_path dirname, basename +(** Add a local installation suffix (unless the suffix is itself + absolute in which case the prefix does not matter) *) +let use_suffix prefix suffix = + if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix + (** A weaker analog of the function in Envars *) 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 + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let coqlib = use_suffix prefix Coq_config.coqlibsuffix in + if Sys.file_exists (coqlib / file) then coqlib else + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file) + then Coq_config.coqlib else prefix let header_trailer = ref true let header_file = ref "" |