diff options
Diffstat (limited to 'tools/Makefile')
| -rw-r--r-- | tools/Makefile | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tools/Makefile b/tools/Makefile index 852f2f4682..e2f3cb26e7 100644 --- a/tools/Makefile +++ b/tools/Makefile @@ -10,8 +10,6 @@ # # ######################################################################### -# $Id: Makefile 12858 2012-08-10 14:45:51Z maranget $ - include Makefile.shared # To make custom toplevels |