On Thu, 6 Apr 2023, Arsen Arsenoviæ wrote:
> maintainer-scripts/ChangeLog:
> 
> 	* update_web_docs_git: Add updated Texinfo to PATH

Do we really need to adjust PATH, or could we just introduce a MAKEINFO 
variable, something like

  if [ x${MAKEINFO}x = xx ]; then
    if [ -x /home/gccadmin/texinfo/install-git/bin/makeinfo ]; then
      MAKEINFO=/home/gccadmin/texinfo/install-git/bin/makeinfo;
    else
      MAKEINFO=makeinfo
    fi
  fi

?

(This also still allows overriding upon invocation.)

Gerald