On Tue, 11 Apr 2023, Arsen Arsenović wrote: > Ah! Good idea. What do you think of the following?
Did you intentionally not implement the following part of my suggestion if [ x${MAKEINFO}x = xx ]; then : that is, allowing to override from the command-line (or crontab)? And why the colons in + : "${MAKEINFO:=${makeinfo_git}/makeinfo}" + : "${TEXI2DVI:=${makeinfo_git}/texi2dvi}" + : "${TEXI2PDF:=${makeinfo_git}/texi2pdf}" ? I don't think we use these elsewhere. Do they serve a purpose or can we omit them and keep things simpler? Please let me know, and I'll see to get this (or probably an updated patch) in place on gcc.gnu.org. Thanks, Gerald