diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-06 12:26:49 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-01-06 13:00:42 +0100 |
commit | 568dffcc32cfdec78e7824fa6875d892fb9cfd5a (patch) | |
tree | 3013a6d58f5b015778445dee15f16d15e35afb15 /plugins | |
parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) |
Remove dir-locals and ship suggested helper hooks instead.
.dir-locals led to issues with unsafe local variable warnings. With
this method the user is opting in to running this code so there are no warnings.
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 4e8830f6c..000000000 --- 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"))))))) |