From 33f19774469f39693abdd90481a931bab3c49b7c Mon Sep 17 00:00:00 2001
From: Andrew Chilton <andychilton@gmail.com>
Date: Thu, 20 Oct 2011 18:45:12 +1300
Subject: [PATCH] Make the default make target do nothing (see
 http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=601935)

---
 Makefile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Makefile b/Makefile
index 27abede..4871c9b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,5 @@
+build:
+
 open:
 	cil summary --is-open
 
-- 
2.39.5