X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fautomake.mk;h=5bdfaa675463a0f85dd55e6e91e6df4b0c3fed29;hb=df43975b759384a68a14a5881feb4673e952587d;hp=976b5845078b62ac76769b071dca2cc1506c80b0;hpb=16c9b320ee7d2d5e57ad15bae865ba603005ef9f;p=pspp

diff --git a/doc/automake.mk b/doc/automake.mk
index 976b584507..5bdfaa6754 100644
--- a/doc/automake.mk
+++ b/doc/automake.mk
@@ -95,3 +95,12 @@ CLEANFILES += pspp-dev.dvi $(docbook_DATA)
 
 doc: $(INFO_DEPS) $(DVIS) $(PDFS) $(PSS) $(HTMLS) $(dist_docbook_DATA)
 PHONY += doc
+
+$(top_srcdir)/doc/help-pages-list: $(UI_FILES)
+	 $(AM_V_GEN)cat $^ | grep '"help[-_]page"' | \
+   $(SED) -e 's% *<property name="help[-_]page">\([^<]*\)</property>%//*[@id='"'"'\1'"'"']%' \
+	-e 's%#%'"'"']/*[@id='"'"'%g' > $@,tmp
+	test -s $@,tmp
+	mv $@,tmp $@
+
+EXTRA_DIST += doc/help-pages-list