On Fri, May 24, 2019 at 10:11:54AM +0200, Jürgen Spitzmüller wrote: > Am Donnerstag, den 23.05.2019, 15:24 +0200 schrieb Pavel Sanda: > > commit 7f125f62d2cfeacdb820aee5ef39f86eb82db3ae > > Author: Pavel Sanda <[email protected]> > > Date: Thu May 23 15:13:27 2019 +0200 > > > > Introduce doc preference for line numbering. > > GUI-wise, I'd suggest not to use a checkable group box, but simply a > checkbox and the line edit right to it.
I'll have a look. BTW since 83a62a6d74d we have extremely wide document settings dialog... Was that intention? Pavel
