For reference, I just updated the URLs. They were pointing to the old mediawiki pages which don't redirect to the new texi2html output.
Thanks (btw, now we are using makeinfo by default, not texi2html).
For reference, I just updated the URLs. They were pointing to the old mediawiki pages which don't redirect to the new texi2html output.
Thanks (btw, now we are using makeinfo by default, not texi2html).