diff options
| author | Jim Meyering <meyering@redhat.com> | 2010-05-03 23:18:40 +0200 |
|---|---|---|
| committer | Jim Meyering <meyering@redhat.com> | 2010-05-03 23:18:40 +0200 |
| commit | 03bc12c7cb9ec501356fdbe9555b145f15e43ace (patch) | |
| tree | be60ffca3fd1533decb27f63b277475575b99e96 /build-aux/gnu-web-doc-update | |
| parent | e6addf84d6331d634b5d76db03f59851f3de8894 (diff) | |
| download | gnulib-03bc12c7cb9ec501356fdbe9555b145f15e43ace.tar.gz | |
gnu-web-doc-update: don't ignore configure or build failure
* build-aux/gnu-web-doc-update: Exit nonzero upon internal failure.
Diffstat (limited to 'build-aux/gnu-web-doc-update')
| -rwxr-xr-x | build-aux/gnu-web-doc-update | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/build-aux/gnu-web-doc-update b/build-aux/gnu-web-doc-update index 2c1a0cc6eb..e834dcf465 100755 --- a/build-aux/gnu-web-doc-update +++ b/build-aux/gnu-web-doc-update @@ -90,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 \ |