Hi Thomas, t...@tsdye.com (Thomas S. Dye) writes:
>> I would mention "make config" here for a sanity check of the created >> configuration. > > Good idea. Done. Oh, I thought it was done in Org's org.texi manual but I understand this is done in orgmanual.git, right? Could you make the change in org.texi too? Thanks! -- Bastien