diff options
Diffstat (limited to 'src/interp/Makefile.in')
| -rw-r--r-- | src/interp/Makefile.in | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/src/interp/Makefile.in b/src/interp/Makefile.in index b222b8da..c7a6b3ce 100644 --- a/src/interp/Makefile.in +++ b/src/interp/Makefile.in @@ -159,23 +159,13 @@ UNUSED= ${DOC}/guess.boot.dvi \ all: all-ax -all-ax: stamp +all-ax: all-interpsys @echo finished $(srcdir) -stamp: remove-stamp build-images - $(STAMP) stamp - -.PHONY: remove-stamp -remove-stamp: - -rm -f stamp - -.PHONY: build-images -build-images: remove-stamp all-interpsys - all-interpsys: $(MAKE) $(SAVESYS) -all-axiomsys: all-interpsys +all-axiomsys: $(MAKE) $(AXIOMSYS) mostlyclean-local: |