X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fautomake.mk;h=52cf9fe61a2c67537dbcc58dbba88902e4fcb4e7;hb=65dea0d51ec33cbc614a3ec87b5aae28c86f005a;hp=63084c5e31b120262cd58247fe71dc710002a6b0;hpb=c8f16e229dede3bf3ec30c329cccc6924778553a;p=pspp
diff --git a/src/ui/gui/automake.mk b/src/ui/gui/automake.mk
index 63084c5e31..52cf9fe61a 100644
--- a/src/ui/gui/automake.mk
+++ b/src/ui/gui/automake.mk
@@ -53,10 +53,11 @@ UI_FILES = \
src/ui/gui/weight.ui
-$(srcdir)/doc/help-pages-list: $(UI_FILES)
- cat $^ | grep '"help-page"' | \
- sed -e 's% *\([^<]*\)%//*[@id='"'"'\1'"'"']%' \
+$(top_srcdir)/doc/help-pages-list: $(UI_FILES)
+ cat $^ | grep '"help[-_]page"' | \
+ $(SED) -e 's% *\([^<]*\)%//*[@id='"'"'\1'"'"']%' \
-e 's%#%'"'"']/*[@id='"'"'%g' > $@
+
EXTRA_DIST += doc/help-pages-list