X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fautomake.mk;h=9844d335d493a709da9afab404ae35f96ab4df27;hb=244ba85cfda15e1d7f98627b4266789cb4fbd4e4;hp=2c6ec860e1266914e74220147987f4e570d280c3;hpb=797066812fea488210d4e43fa6c7ee97c08fd0f6;p=pspp

diff --git a/doc/automake.mk b/doc/automake.mk
index 2c6ec860e1..9844d335d4 100644
--- a/doc/automake.mk
+++ b/doc/automake.mk
@@ -81,8 +81,8 @@ $(srcdir)/doc/pspp.xml: doc/pspp.texi $(doc_pspp_TEXINFOS) doc/help-pages-list
 	 | $(AWK) '/<para>.*<table.*>.*<\/para>/{x=sub("</para>",""); print; s=1;next}/<\/table>/{print; if (s==1) print "</para>"; s=0; next}1' \
 	> $@,tmp
 	$(AM_V_at)$(XMLLINT) --output /dev/null $@,tmp
-	cat doc/help-pages-list | while read node ; do \
-	 $(AM_V_at)$(XMLLINT) --xpath "$$node" $@,tmp > /dev/null; \
+	$(AM_V_at)cat doc/help-pages-list | while read node ; do \
+	 $(XMLLINT) --xpath "$$node" $@,tmp > /dev/null; \
 	 if test $$? -ne 0 ; then  echo "$$node does not appear in $@" ; exit 1; fi ; \
 	 done 
 	mv $@,tmp $@