diff options
Diffstat (limited to 'Makefile.pamphlet')
| -rw-r--r-- | Makefile.pamphlet | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile.pamphlet b/Makefile.pamphlet index 8f1a82b6..3bd131cb 100644 --- a/Makefile.pamphlet +++ b/Makefile.pamphlet @@ -340,6 +340,10 @@ endif $(AXIOM_SRC_TARGETS): cd "$(build_srcdir)" && $(MAKE) $@ +.PHONY: all-algstrap +all-algstrap: + cd src/algebra && $(MAKE) $@ + <<rootdirs>> <<noweb>> |