aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-13 15:26:40 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-13 15:33:29 +0100
commitfbe9d252ef31f49a75225b8c71be56a38bc51a3d (patch)
tree353439e11925173358a8d9beff1035d15795283c /dev/tools
parent9997f9aec01abdb59852ec5706ef36ce56311109 (diff)
coqdev.el: shell-quote-argument the directory for make -C
Diffstat (limited to 'dev/tools')
-rw-r--r--dev/tools/coqdev.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 20613a4cf..01334690c 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -39,7 +39,7 @@
(defun coqdev-setup-compile-command ()
"Setup `compilate-command' for Coq development."
(let ((dir (coqdev-default-directory)))
- (when dir (setq-local compile-command (concat "make -C " dir)))))
+ (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir))))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
(defvar camldebug-command-name) ; from camldebug.el (caml package)