diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-06-21 13:49:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-01 19:26:33 +0200 |
| commit | c720b6f20a4bef54c570d9a3002938828779654b (patch) | |
| tree | ab0e43050a1a59c003cb3e2c868b2ea97683c02a /dev/README | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Remove unused Makefiles in dev/tools/
They seem unused since 8f4b7f1 (2007).
Diffstat (limited to 'dev/README')
| -rw-r--r-- | dev/README | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/dev/README b/dev/README index 814f60957..b446c3e97 100644 --- a/dev/README +++ b/dev/README @@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- -Makefile.dir: makefile dedicated to intensive work in a given directory -Makefile.subdir: makefile dedicated to intensive work in a given subdirectory -Makefile.devel: utilities to automatically launch coq in various states -Makefile.common: used by other Makefiles 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 |