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 | |
| 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.
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 4 | ||||
| -rw-r--r-- | test-suite/Makefile | 14 |
3 files changed, 10 insertions, 10 deletions
diff --git a/configure.ml b/configure.ml index 6e15cdbe4e..55d71f6c2e 100644 --- a/configure.ml +++ b/configure.ml @@ -975,7 +975,7 @@ let config_runtime () = | Some flags -> string_split ',' flags | _ when use_custom -> [custom_flag] | _ when !prefs.local -> - ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"] + ["-dllib";"-lcoqrun";"-dllpath";("\"" ^ coqtop ^ "/kernel/byterun\"")] | _ -> let ld="CAML_LD_LIBRARY_PATH" in build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld; 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 diff --git a/test-suite/Makefile b/test-suite/Makefile index 265c2eafa7..6a6b729578 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -33,10 +33,10 @@ include ../Makefile.common ####################################################################### ifneq ($(wildcard ../_build),) -BIN:=$(shell cd ..; pwd)/_build/install/default/bin/ -COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq +BIN:='$(shell cd ..; pwd)'/_build/install/default/bin/ +COQLIB:='$(shell cd ..; pwd)'/_build/install/default/lib/coq else -BIN := $(shell cd ..; pwd)/bin/ +BIN := '$(shell cd ..; pwd)'/bin/ COQLIB?= ifeq ($(COQLIB),) @@ -602,10 +602,10 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - export BIN="$(BIN)"; \ - export coqc="$(coqc)"; \ - export coqtop="$(coqc)"; \ - export coqdep="$(coqdep)"; \ + export BIN=$(BIN); \ + export coqc="eval $(coqc)"; \ + export coqtop="eval $(coqc)"; \ + export coqdep="eval $(coqdep)"; \ "$<" 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ |