Commit 22f880ff9b1cc1cef82a2924ab650c7c2bbbe46b
2021-01-09T11:42:26
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.