diff options
| author | Hugo Herbelin | 2020-02-28 23:08:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-28 23:08:05 +0100 |
| commit | 7c1d1a58697486f4f52ac7f45b932d03a7e77e5c (patch) | |
| tree | ce4a5f8cbd17e9dcaed5202b43d946b8a6e1e52d /ide | |
| parent | c2d7fbe834031a45e3be4c5cdf93694e109131e9 (diff) | |
| parent | 7462ca3189ceff514bdb919ae7f2908d0f0c0518 (diff) | |
Merge PR #10008: CoqIDE: Fix not escaping coqtop arguments when compiling
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
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 |