diff options
Diffstat (limited to 'tools/verification/rv/Makefile')
| -rw-r--r-- | tools/verification/rv/Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile index 5b898360ba48..8ae5fc0d1d17 100644 --- a/tools/verification/rv/Makefile +++ b/tools/verification/rv/Makefile @@ -78,4 +78,7 @@ clean: doc_clean fixdep-clean $(Q)rm -f rv rv-static fixdep FEATURE-DUMP rv-* $(Q)rm -rf feature -.PHONY: FORCE clean +check: $(RV) + RV=$(RV) prove -o --directives -f tests/ + +.PHONY: FORCE clean check |