diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-12-15 17:04:09 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-12-21 23:22:46 +0000 |
commit | 857831d18708ada4590c511494d3ae5f94cf6a6a (patch) | |
tree | 227f3e2c511e302eafef996f4f1fa763ddbe427a /Makefile | |
parent | 48897e2aa072fa75ae6046b848ae14c7b056c29a (diff) | |
download | klee-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" )
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 6 |
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 |