diff options
Diffstat (limited to 'src/Makefile.pamphlet')
| -rw-r--r-- | src/Makefile.pamphlet | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Makefile.pamphlet b/src/Makefile.pamphlet index 06029371..f2f86358 100644 --- a/src/Makefile.pamphlet +++ b/src/Makefile.pamphlet @@ -246,17 +246,20 @@ subdir = src/ SUBDIRS = @axiom_src_subdirs@ -.PHONY: all all-ax all-src all-clef all-sman +.PHONY: all all-ax all-src all-clef all-sman all-driver all: all-ax all-ax all-src: stamp @echo finished $(builddir) -stamp: @axiom_src_all@ +stamp: @axiom_src_all@ all-driver -rm -f stamp $(STAMP) stamp +all-driver: + @cd driver && $(MAKE) $@ + <<clefdir>> <<smandir>> <<hyperdir>> |