diff options
Diffstat (limited to 'src/input/Makefile.pamphlet')
| -rw-r--r-- | src/input/Makefile.pamphlet | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/input/Makefile.pamphlet b/src/input/Makefile.pamphlet index 484e1501..6b673e35 100644 --- a/src/input/Makefile.pamphlet +++ b/src/input/Makefile.pamphlet @@ -52,7 +52,7 @@ regress target. <<genericRules>>= ${OUT}/%.input: %.input - @ $(INSTALL) $< $@ + @cp -p $< $@ .PRECIOUS: %.input @@ -60,7 +60,7 @@ ${OUT}/%.input: %.input @$(axiom_build_document) --output=$@ --tangle $< ${OUT}/%.as: %.as - @ $(INSTALL) $< $@ + @cp -p $< $@ %.as: ${IN}/%.as.pamphlet @ $(axiom_build_document) --output=$@ --tangle $< @@ -878,7 +878,7 @@ all-ax all-input: $(OUT) ${FILES} ${FILES2} ${ASFILES} @echo 1 finished $(srcdir) $(OUT): - $(mkinstalldirs) $@ + $(mkdir_p) $@ <<genericRules>> |