diff options
Diffstat (limited to 'src/etc')
| -rw-r--r-- | src/etc/Makefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/etc/Makefile.in b/src/etc/Makefile.in index b642bda1..c06c0437 100644 --- a/src/etc/Makefile.in +++ b/src/etc/Makefile.in @@ -109,7 +109,7 @@ asq$(EXEEXT): $(asq_objects) asq.c: $(srcdir)/asq.c.pamphlet - $(axiom_build_document) --tangle --output=$@ $< + $(oa_hammer) --tangle --output=$@ $< $(axiom_target_libdir)/summary: $(srcdir)/summary cp -p $< $@ |