diff options
Diffstat (limited to 'tools/klee-stats')
| -rw-r--r-- | tools/klee-stats/Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/klee-stats/Makefile b/tools/klee-stats/Makefile index 0b35fa51..89578b12 100644 --- a/tools/klee-stats/Makefile +++ b/tools/klee-stats/Makefile @@ -11,6 +11,10 @@ LEVEL = ../.. TOOLSCRIPTNAME := klee-stats +# 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. |