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/include | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Remove unused Makefiles in dev/tools/
They seem unused since 8f4b7f1 (2007).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions