aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-24 09:32:10 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-24 09:32:10 +0100
commita470526e00d853abb5b89ea61a7c55f952204d68 (patch)
tree6379b627f22526825d6f491accd5052df8b79744 /dev
parent89bd76b6f6a534613b03aaa970baf513b7c9b76b (diff)
parent6938d81c37467073d0bd731c0ef9e3feed92fb2f (diff)
Merge PR #6803: coqdev.el: add space at the end of compile-command
Diffstat (limited to 'dev')
-rw-r--r--dev/tools/coqdev.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 8c55be283..62fdaec80 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -39,7 +39,8 @@
(defun coqdev-setup-compile-command ()
"Setup `compile-command' for Coq development."
(let ((dir (coqdev-default-directory)))
- (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir))))))
+ ;; we add a space at the end to make it easy to add arguments (eg -j or target)
+ (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)