From 568dffcc32cfdec78e7824fa6875d892fb9cfd5a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 6 Jan 2018 12:26:49 +0100
Subject: 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.
---
 dev/README | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev/README')

diff --git a/dev/README b/dev/README
index b446c3e974..f97e2a7690 100644
--- a/dev/README
+++ b/dev/README
@@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
 Other development tools (directory tools)
 -----------------------
 
+coqdev.el: helper customizations for everyday Coq development, eg
+  making `compile' work in subdirectories
+
 objects.el: various development utilities at emacs level
+
 anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
   location of Anomaly backtraces and jump to them conveniently from
   the Emacs *compilation* output.
-- 
cgit v1.2.3