Why are there uncommitted changes to update_web_docs_git on the server?

[Jonathan Wakely]

I have decided from the date on the file and the logins that happened
that day, that it was probably Gerald.

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

On Tue, 16 Dec 2025 at 13:55, Jonathan Wakely <jwakely.gcc@gmail.com> wrote:
>
> --- a/maintainer-scripts/update_web_docs_git
> +++ b/maintainer-scripts/update_web_docs_git
> @@ -307,6 +307,13 @@ find jit $LIBGDIAGNOSTICS \
>     -o -name "*.css" -o -name "*.js" \
>     -o -name "*.txt" |
>   while read file ; do
> +    case $file in
> +      *.html)
> +        sed -e 's#<a
> href="https://github.com/bitprophet/alabaster">Alabaster
> 0.7.12</a>#Alabaster#' \
> +            -e 's#<a href="http://sphinx-doc.org/">Sphinx 5.3.0</a>#Sphinx#' \
> +            -i $file
> +       ;;
> +    esac
>     # Note that $file here will contain path fragments beginning
>     # with "jit/", e.g. "jit/cp/topics/functions.html"
>     mkdir -p $(dirname $DOCSDIR/$file)
>
> It looks like somebody edited this file in August, but the changes
> should be committed to Git not just edited in place in that checkout.