From 02b40f6cdb7ec56f34c6b773b1d7768b4b135fd9 Mon Sep 17 00:00:00 2001
From: Ike Mulder
Date: Fri, 26 Apr 2019 16:16:47 +0200
Subject: 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.
---
 ide/coqide.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3