X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pspp;a=blobdiff_plain;f=src%2Fui%2Fgui%2Fautomake.mk;h=82590e6e1a6ba1918cd857b8b8e995b1c31b8e0e;hp=10b315061a05973db6b05125824ab22c8b0be78e;hb=6b55442545f78ac54922e1a5b080b87b2b65f28c;hpb=317c8374ac805fd00048a6e2baefcdf72b9e50c2

diff --git a/src/ui/gui/automake.mk b/src/ui/gui/automake.mk
index 10b315061a..82590e6e1a 100644
--- a/src/ui/gui/automake.mk
+++ b/src/ui/gui/automake.mk
@@ -54,7 +54,7 @@ UI_FILES = \
 
 
 $(top_srcdir)/doc/help-pages-list: $(UI_FILES)
-	 cat $^ | grep '"help[-_]page"' | \
+	 $(AM_V_GEN)cat $^ | grep '"help[-_]page"' | \
    $(SED) -e 's% *<property name="help[-_]page">\([^<]*\)</property>%//*[@id='"'"'\1'"'"']%' \
 	-e 's%#%'"'"']/*[@id='"'"'%g' > $@