diff options
Diffstat (limited to 'build-aux/gnu-web-doc-update')
| -rwxr-xr-x | build-aux/gnu-web-doc-update | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/build-aux/gnu-web-doc-update b/build-aux/gnu-web-doc-update index c041364fb..c968b1dcd 100755 --- a/build-aux/gnu-web-doc-update +++ b/build-aux/gnu-web-doc-update @@ -4,7 +4,7 @@ VERSION=2022-01-27.18; # UTC -# Copyright (C) 2009-2022 Free Software Foundation, Inc. +# Copyright (C) 2009-2023 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 @@ -153,8 +153,8 @@ cleanup() $GIT branch -d $tmp_branch exit $__st } -trap cleanup 0 -trap 'exit $?' 1 2 13 15 +trap cleanup EXIT +trap 'exit $?' HUP INT PIPE TERM # We must build using sources for which --version reports the # just-released version number, not some string like 7.6.18-20761. |