aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-12 07:33:19 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-12 07:33:41 +0100
commita6d048a2de62bba97948fee2937dc5ea2fad0c83 (patch)
tree09a8d0b144fa6b459676180b1bfc1132e6b3a6b5 /dev/tools
parent10e3c8e59664ed5137cd650ba6e0704943c511e8 (diff)
Removing an empty file detected by Luc Grateau.
Diffstat (limited to 'dev/tools')
-rw-r--r--dev/tools/Makefile.common0
1 files changed, 0 insertions, 0 deletions
diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common
deleted file mode 100644
index e69de29bb..000000000
--- a/dev/tools/Makefile.common
+++ /dev/null