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/coq_makefile.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 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 78c92e68b..8e2f75fc9 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -119,14 +119,8 @@ let read_whole_file s = Buffer.contents b let makefile_template = - let open Filename in let template = "/tools/CoqMakefile.in" in - if Coq_config.local then - let coqbin = CUnix.canonical_path_name (dirname Sys.executable_name) in - dirname coqbin ^ template - else match Coq_config.coqlib with - | None -> assert false - | Some dir -> dir ^ template + Coq_config.coqlib ^ template let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s |