Akim Demaille wrote: > > Le 15 sept. 2022 à 19:02, Jacob L. Mandelson <jlm-bbi...@jlm.ofb.net> a > > écrit : > > > > I think the English text needs a few minor edits.[...] > > Thanks a lot for this! I installed the following commit, with your fixes.
Thanks. It looks good; I can't easily test it now, but after the next release (but don't bother making one just for this). > +@deffn Directive {%define cex.timeout} @var{duration} Does this mean this can be set in the grammar file? I wonder if that's useful -- it seems more of an environmental setting to me. But if it would be more work to make it not settable this way, don't worry.