From: John Darrington <john@darrington.wattle.id.au>
Date: Sun, 21 Aug 2016 12:29:21 +0000 (+0200)
Subject: Ensure that help page manifest is not empty.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=5c0ec34670a7d9cfb1abc4cd5b25ccb88de3cbee;p=pspp

Ensure that help page manifest is not empty.

For some reason I have found that sometimes doc/help-pages-list
is zero bytes long.   I don't know how this happens, but this
change should catch it and allow us to find out why.
---

diff --git a/src/ui/gui/automake.mk b/src/ui/gui/automake.mk
index e991eb2e47..3f3303fc14 100644
--- a/src/ui/gui/automake.mk
+++ b/src/ui/gui/automake.mk
@@ -54,7 +54,9 @@ UI_FILES = \
 $(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' > $@
+	-e 's%#%'"'"']/*[@id='"'"'%g' > $@,tmp
+	test -s $@,tmp
+	mv $@,tmp $@
 
 EXTRA_DIST += doc/help-pages-list