diff options
| author | Maxime Dénès | 2018-02-19 10:07:23 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-19 10:07:23 +0100 |
| commit | 8e9d1421354d55bc2ea71e37715a19d33cc9bc9c (patch) | |
| tree | ec38dd5eac6843ce61e3e499a359eb103f15cb3d /plugins | |
| parent | 2a47eae1c4556a34ecf91a27f756e299dfe18a98 (diff) | |
| parent | d9cb50d8f9b2bb16ddf7c27c146e09d7de33b90f (diff) | |
Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/.dir-locals.el | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el deleted file mode 100644 index 4e8830f6c1..0000000000 --- a/plugins/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) |