diff options
| author | Enrico Tassi | 2017-07-17 18:05:34 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-07-20 15:44:13 +0200 |
| commit | ad8bf70ccc61849cfb1ade20ce426ea2ec74aa0e (patch) | |
| tree | 3513182351b72746e870d9e0ecfdce4a1c432c58 /tools/coq_makefile.ml | |
| parent | 1fd1ca0703811392c890c41a796ed7efdaacca28 (diff) | |
coq-makefile: strip windows drive letter when DESTDIR is not empty
In unix one can concatenate a prefix with an absolute path in
order to obtain a valid path. This is not the case on Windows.
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0e0375c008..327f53520c 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -193,12 +193,19 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) ;; +let windrive s = + if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0) + then Str.matched_string s + else s +;; + let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; + fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; let generate_conf_files oc |