X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=build-aux%2Fgnu-web-doc-update;h=f6d0ee1f4e73eddb57195ac608e18d610f54badd;hb=001e7d63dfe613e249e9f4ab53170b401532afd3;hp=adf6c5179cfda1747a8ba96aa79a0d26a754b28e;hpb=faf52e824a51a93d173ed97c8901415a0be19481;p=pspp

diff --git a/build-aux/gnu-web-doc-update b/build-aux/gnu-web-doc-update
index adf6c5179c..f6d0ee1f4e 100755
--- a/build-aux/gnu-web-doc-update
+++ b/build-aux/gnu-web-doc-update
@@ -9,7 +9,7 @@
 
 VERSION=2009-07-21.16; # UTC
 
-# Copyright (C) 2009 Free Software Foundation, Inc.
+# Copyright (C) 2009-2011 Free Software Foundation, Inc.
 
 # This program is free software: you can redistribute it and/or modify
 # it under the terms of the GNU General Public License as published by
@@ -37,8 +37,9 @@ help_version()
     --help) cat <<EOF
 Usage: $ME
 
-Output a list of version-controlled files in DIR (default .), relative to
-SRCDIR (default .).  SRCDIR must be the top directory of a checkout.
+Run this script (no options or arguments) after each non-alpha release,
+to update the web documentation at http://www.gnu.org/software/\$pkg/manual/
+Run it from your project's the top-level directory.
 
 Options:
   --help     print this help, then exit
@@ -89,7 +90,9 @@ trap 'exit $?' 1 2 13 15
 # just-released version number, not some string like 7.6.18-20761.
 # That version string propagates into all documentation.
 git checkout -b $tmp_branch v$version
-./bootstrap && ./configure && make && make web-manual
+ok=0
+./bootstrap && ./configure && make && make web-manual && ok=1
+test $ok = 1 || exit 1
 
 tmp=$(mktemp -d --tmpdir=. web-doc-update.XXXXXX) || exit 1
 ( cd $tmp \