aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2017-07-17 10:51:45 +0200
committerEnrico Tassi2017-07-20 15:40:48 +0200
commit2065b2abcc4fd42345ab9bfdafd75cf2a5a0889d (patch)
tree7bd6e5a1b1aa834ad48981911dd4c4cb88168c15
parent7f7075d10780fe24c97e329868a501c2af422625 (diff)
coq-makefile: quote using ' to preserve \ (windows paths)
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c3aedf538e..c76b68dab3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -118,7 +118,7 @@ let makefile_template =
let template = "/tools/CoqMakefile.in" in
Coq_config.coqlib ^ template
-let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s
+let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s
let generate_makefile oc conf_file local_file args project =
let s = read_whole_file makefile_template in