diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-12 07:33:19 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-12 07:33:41 +0100 |
commit | a6d048a2de62bba97948fee2937dc5ea2fad0c83 (patch) | |
tree | 09a8d0b144fa6b459676180b1bfc1132e6b3a6b5 /dev/tools | |
parent | 10e3c8e59664ed5137cd650ba6e0704943c511e8 (diff) |
Removing an empty file detected by Luc Grateau.
Diffstat (limited to 'dev/tools')
-rw-r--r-- | dev/tools/Makefile.common | 0 |
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 |