diff options
Diffstat (limited to 'build-aux/gnu-web-doc-update')
| -rwxr-xr-x | build-aux/gnu-web-doc-update | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/build-aux/gnu-web-doc-update b/build-aux/gnu-web-doc-update index 1684f5e5b5..ec2116852c 100755 --- a/build-aux/gnu-web-doc-update +++ b/build-aux/gnu-web-doc-update @@ -2,7 +2,7 @@ # Run this after each non-alpha release, to update the web documentation at # http://www.gnu.org/software/$pkg/manual/ -VERSION=2016-01-11.22; # UTC +VERSION=2016-01-12.23; # UTC # Copyright (C) 2009-2016 Free Software Foundation, Inc. @@ -117,7 +117,7 @@ do opt=$(echo "$1" | sed -e 's/=.*//') val=$(echo "$1" | sed -e 's/[^=]*=//') shift - set dummy "$opt" "$val" ${1+"$@"}; shift + set dummy "$opt" "$val" "$@"; shift ;; esac |