about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2013-12-15 17:04:09 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2013-12-21 23:22:46 +0000
commit857831d18708ada4590c511494d3ae5f94cf6a6a (patch)
tree227f3e2c511e302eafef996f4f1fa763ddbe427a
parent48897e2aa072fa75ae6046b848ae14c7b056c29a (diff)
downloadklee-857831d18708ada4590c511494d3ae5f94cf6a6a.tar.gz
Do not install KLEE's header files. They are not for public
consumption.

The header files are normally installed
by the install-local target in the top-level
makefile.

See Makefile.rules ( "Install support for the project's include files" )
-rw-r--r--Makefile6
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 1612efc1..2e02e578 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,12 @@ LEVEL = .
 
 include $(LEVEL)/Makefile.config
 
+# The header files are normally installed
+# by the install-local target in the top-level
+# makefile. This disables installing anything
+# in the top-level makefile.
+NO_INSTALL=1
+
 DIRS = lib tools runtime
 EXTRA_DIST = include