diff options
-rw-r--r-- | test/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/Makefile b/test/Makefile index bfdeb16d..6372d512 100644 --- a/test/Makefile +++ b/test/Makefile @@ -47,9 +47,10 @@ endif LIT_ALL_TESTSUITES := $(LIT_TESTSUITE) check-local:: lit.site.cfg + $(Verb) $(MAKE) -s clean $(Verb) ( $(ULIMIT) \ $(PYTHON) $(LLVM_SRC_ROOT)/utils/lit/lit.py $(LIT_ARGS) $(LIT_TESTSUITE) ) - @klee_last_path=$$(find . -name klee-last | head -1); \ + $(Verb) klee_last_path=$$(find . -name klee-last | head -1); \ if [ ! -z "$$klee_last_path" ]; then \ echo "error: one of the tests failed to use --output-dir, found: $$klee_last_path"; \ exit 1; \ |