diff options
Diffstat (limited to 'Makefile.pamphlet')
| -rw-r--r-- | Makefile.pamphlet | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Makefile.pamphlet b/Makefile.pamphlet index 80ecd2ba..cd6fcca2 100644 --- a/Makefile.pamphlet +++ b/Makefile.pamphlet @@ -345,6 +345,11 @@ $(AXIOM_SRC_TARGETS): <<gcl>> <<install>> +.PHONY: check +check: + cd src && $(MAKE) all-check + + mostlyclean-local: @-rm -f lastBuildDate |