diff --git a/share/Makefile.testing b/share/Makefile.testing index 3569f03d45e3eb5819b961344a60ee4dff7efeac..e7fae696d932676377473f5b3efdd4f2933dc7fa 100644 --- a/share/Makefile.testing +++ b/share/Makefile.testing @@ -204,6 +204,11 @@ tests:: endif # FRAMAC_WP_CACHEDIR endif # PTEST_USE_WP_CACHE +.PHONY: default-tests +default-tests: run-ptests + dune build --display short @ptests_config + $(MAKE) count-tests + .PHONY: count-tests count-tests: @echo "Number of *.{err,res}.log files:"