diff options
| -rw-r--r-- | tools/klee-stats/Makefile | 4 | ||||
| -rw-r--r-- | tools/ktest-tool/Makefile | 4 |
2 files changed, 8 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. 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. |