diff options
| author | Ike Mulder | 2019-04-26 16:16:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-28 05:35:56 +0100 |
| commit | 02b40f6cdb7ec56f34c6b773b1d7768b4b135fd9 (patch) | |
| tree | a36dd7ef9fd751bdeb7a4fbfd4add4ed4d68c2b6 /ide | |
| parent | aeca986089d005054496ed4bcf1b920e8fa02173 (diff) | |
Fixed some escaping problems with arguments containing spaces in IDE's Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 143a12deeb..61e95c21b1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -460,7 +460,7 @@ let compile sn = |Some f -> let args = Coq.get_arguments sn.coqtop in let cmd = cmd_coqc#get - ^ " " ^ String.concat " " args + ^ " " ^ String.concat " " (List.map Filename.quote args) ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in @@ -474,7 +474,7 @@ let compile sn = flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); - sn.messages#default_route#set (Pp.str "Compilation output:\n"); + sn.messages#default_route#set (Pp.str ("Compilation output:\n" ^ cmd ^ "\n")); sn.messages#default_route#add (Pp.str (Buffer.contents buf)); end in |