diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:32:10 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:32:10 +0100 |
| commit | a470526e00d853abb5b89ea61a7c55f952204d68 (patch) | |
| tree | 6379b627f22526825d6f491accd5052df8b79744 /dev | |
| parent | 89bd76b6f6a534613b03aaa970baf513b7c9b76b (diff) | |
| parent | 6938d81c37467073d0bd731c0ef9e3feed92fb2f (diff) | |
Merge PR #6803: coqdev.el: add space at the end of compile-command
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/tools/coqdev.el | 3 |
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) |