diff options
| author | letouzey | 2012-08-06 14:42:57 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-06 14:42:57 +0000 |
| commit | 335a3d971e9cc5d9f3365126f7a78a8d0c1007e3 (patch) | |
| tree | 909b9911c5fafbc65a2be83b9a01e919c5f61e7f | |
| parent | cf692701443d1ea7f7d2c1b06dea56d6052bd58d (diff) | |
Win32: some quote fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15688 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 8 |
2 files changed, 9 insertions, 5 deletions
diff --git a/Makefile.build b/Makefile.build index db977cb13f..7fa1d992d2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -529,9 +529,9 @@ $(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BEST ifeq ($(CAMLP4),camlp4) tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< else tools/compat5.cmo: tools/compat5.ml $(OCAMLC) -c $< @@ -725,7 +725,7 @@ dev/printers.cma: | dev/printers.mllib.d grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index bd4dec2b6f..51c3fbb942 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -260,14 +260,14 @@ let main () = if !opt then begin (* native code *) if !top then failwith "no custom toplevel in native code !"; - let ocamloptexec = Filename.concat camlbin "ocamlopt" in + let ocamloptexec = Filename.quote (Filename.concat camlbin "ocamlopt") in ocamloptexec^" -linkall" end else (* bytecode (we shunt ocamlmktop script which fails on win32) *) let ocamlmktoplib = if is_ocaml4 then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma" else " toplevellib.cma" in - let ocamlcexec = Filename.concat camlbin "ocamlc" in + let ocamlcexec = Filename.quote (Filename.concat camlbin "ocamlc") in let ocamlccustom = Printf.sprintf "%s %s -linkall " ocamlcexec Coq_config.coqrunbyteflags in (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom) @@ -290,6 +290,10 @@ let main () = let args = if !top then args @ [ "topstart.cmo" ] else args in (* Now, with the .cma, we MUST use the -linkall option *) let command = String.concat " " (prog::"-rectypes"::args) in + (* In Win32, when Sys.command (and hence cmd.exe) executes a command + that may contains many double-quote, we should double-quote the whole ! *) + let command = if Sys.os_type = "Win32" then "\""^command^"\"" else command + in if !echo then begin print_endline command; |