From c720b6f20a4bef54c570d9a3002938828779654b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 21 Jun 2017 13:49:15 +0200
Subject: Remove unused Makefiles in dev/tools/

They seem unused since 8f4b7f1 (2007).
---
 dev/README | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'dev/README')

diff --git a/dev/README b/dev/README
index 814f609576..b446c3e974 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
-- 
cgit v1.2.3