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/tools/Makefile.subdir | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 dev/tools/Makefile.subdir

(limited to 'dev/tools/Makefile.subdir')

diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir
deleted file mode 100644
index cb914bd129..0000000000
--- a/dev/tools/Makefile.subdir
+++ /dev/null
@@ -1,7 +0,0 @@
-# if you work in a sub/sub-rectory of Coq
-# you should make a link to that makefile 
-#    ln -s ../../dev/tools/Makefile.subdir Makefile
-# in order to have all the facilities of dev/tools/Makefile.dir
-
-TOPDIR=../..
-include $(TOPDIR)/dev/tools/Makefile.dir
-- 
cgit v1.2.3