Hi Nicolas, 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.
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? I'd rather make the switch now so that users and contributors are not confused by the presence of two manuals in the repo. Thanks, -- Bastien
