aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml8
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