Allow setting CVS username for gnu-web-doc-update.
commit22f880ff9b1cc1cef82a2924ab650c7c2bbbe46b
authorDarshit Shah <darnir@gnu.org>
Sat, 9 Jan 2021 10:42:26 +0000 (9 11:42 +0100)
committerBruno Haible <bruno@clisp.org>
Sat, 9 Jan 2021 14:20:40 +0000 (9 15:20 +0100)
treec91a7eadec54b84df4149067308fb77c58e14b0a
parent8ed1d1f9f4a4f1b5ae76f1f0440813f4e895280a
Allow setting CVS username for gnu-web-doc-update.

* build-aux/gnu-web-doc-update: Introduce new option --user to set the
name of the user on Savannah, when it doesn't match $USER.
ChangeLog
build-aux/gnu-web-doc-update