Why are there uncommitted changes to update_web_docs_git on the server?

[Gerald Pfeifer]

On Wed, 17 Dec 2025, Jonathan Wakely wrote:
> I have decided from the date on the file and the logins that happened
> that day, that it was probably Gerald.

And Gerald pleads guilty. My bad!

> Gerald, should this change be committed to git or can it be discarded?

I put this in place to avoid a number of bad redirects (after raising 
these without resolution IIRC). And apparently, and embarrassingly, missed 
pushing it properly after verifying its function.

Fixed now.

Gerald