Hello, Bastien <b...@gnu.org> writes:
> it would be nice to make the switch to org-manual.org for Org 9.2, > and to delete org.texi entirely from the master branch. Done. > I guess we need to add some Makefile rules so that "make pdf" first > exports .org => .texi then exports .texi to .pdf... is that so? Done (or so I think). Regards, -- Nicolas Goaziou 0x80A93738
