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