On 2016-11-23, Scott Kostyshak wrote: > [-- Type: text/plain, Encoding: quoted-printable --]
> On Tue, Nov 22, 2016 at 08:54:05AM +0000, Guenter Milde wrote: >> Therefore: >> * Warn the user when including a child document with different >> "use-non-TeX-fonts" setting. > +1. It would be simliar to what we do if the document class of the child > is different from master. Yes. Could you implement this or file a bug report at track? Thanks Günter
