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 <[email protected]> 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.
