diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-21 11:52:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-21 11:52:31 +0100 |
| commit | 6938d81c37467073d0bd731c0ef9e3feed92fb2f (patch) | |
| tree | 1afddd5dbe1fdf90b87d937f10954d273e879419 /dev/tools | |
| parent | aec63ba9c8f6840d98ba731640a786138d836343 (diff) | |
coqdev.el: add space at the end of compile-command
That way you can just type [-j] instead of having to remember to add a
space yourself.
Diffstat (limited to 'dev/tools')
| -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) |