| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-06 | Remove dir-locals and ship suggested helper hooks instead. | Gaƫtan Gilbert | |
| .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. | |||
| 2017-05-18 | Add .dir-locals.el to plugins | Jason Gross | |
| As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542 | |||
