diff options
| author | Gaëtan Gilbert | 2017-06-21 13:49:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-08-01 19:26:33 +0200 |
| commit | c720b6f20a4bef54c570d9a3002938828779654b (patch) | |
| tree | ab0e43050a1a59c003cb3e2c868b2ea97683c02a /dev/tools/Makefile.subdir | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Remove unused Makefiles in dev/tools/
They seem unused since 8f4b7f1 (2007).
Diffstat (limited to 'dev/tools/Makefile.subdir')
| -rw-r--r-- | dev/tools/Makefile.subdir | 7 |
1 files changed, 0 insertions, 7 deletions
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 |