Hi Collin,
> Any thoughts on this change?
Writing generally useful software means to _reduce_ assumptions,
not to add assumptions.
Each time you add an assumption, it should raise a red flag for you.
In this case, your patch adds not only one, but two assumptions:
1) That the git repository hoster uses the same user name as
the savannah CVS.
This assumption is already known to be invalid in some cases:
Some GNU packages are hosted on codeberg.org or gitlab.com.
2) That the user has listed their user names per host in ~/.ssh/config.
This assumption is also invalid in some cases:
For me as a user, for example.
Therefore I would forget about the patch and think about the
original problem again:
> my local system username is
> "collin", but my Savannah username is "collinfunk".
The gnu-web-doc-update script has an option --user for this purpose.
What prevents you to use this option, is
> When I first ran 'make web-manual-update'
... the use from a Makefile. So what you would need here is an
environment variable, not an option.
> I had to run
> 'USER=collinfunk make web-manual-update', which worked fine.
But that is not a good solution: $USER has an effect on many programs,
not only on 'cvs' or this particular use of 'cvs'.
So, here is my take on it: Add an environment variable, different from 'USER',
as an alternative to --user.
Bruno
