aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/README
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-01-06 12:26:49 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-01-06 13:00:42 +0100
commit568dffcc32cfdec78e7824fa6875d892fb9cfd5a (patch)
tree3013a6d58f5b015778445dee15f16d15e35afb15 /dev/README
parent2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (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 'dev/README')
-rw-r--r--dev/README4
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/README b/dev/README
index b446c3e97..f97e2a769 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.