diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-01-09 16:38:28 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-01-09 16:38:28 +0000 |
| commit | 8754d26cc5e1558f4dd9c55ad7129e2ad4189fdb (patch) | |
| tree | 757ed906658da6b2a4f0bdaf940af7fe4c9ab74d /tools/ktest-tool | |
| parent | c26accf1c3fe572fdcb5e21d74857b836df1efbf (diff) | |
| download | klee-8754d26cc5e1558f4dd9c55ad7129e2ad4189fdb.tar.gz | |
Fix build system so that ktest-tool and klee-stats can be installed
under release build. The problem is that under release build the install command is told to strip symbols from the tools. It tries to do this for the python scripts and fails. This commit hacks this by requesting that symbols are not stripped from the python scripts.
Diffstat (limited to 'tools/ktest-tool')
| -rw-r--r-- | tools/ktest-tool/Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/ktest-tool/Makefile b/tools/ktest-tool/Makefile index 69d7324c..580b1f6a 100644 --- a/tools/ktest-tool/Makefile +++ b/tools/ktest-tool/Makefile @@ -11,6 +11,10 @@ LEVEL = ../.. TOOLSCRIPTNAME := ktest-tool +# Hack to prevent install trying to strip +# symbols from a python script +KEEP_SYMBOLS := 1 + include $(LEVEL)/Makefile.common # FIXME: Move this stuff (to "build" a script) into Makefile.rules. |