Re: [ jEdit-devel ] Line numbers in the gutter

[Shlomy R. <sre...@gm...>]

On Wed, Apr 22, 2009 at 5:54 PM, Kazutoshi Satoda
<k_s...@f2...> wrote:
> Shlomy Reinstein wrote:
>>>
>>> Could you please make the minimal number of digits configurable?
>
> (snip)
>>
>> Committed into SVN rev 14973, you can now control the minimal number
>> of digits using Global Options -> Gutter, just below line numbering.
>
> Thank you for the fast adoption.
>
> I tried r14973, and found that the minimum width is not changed when I
> set the new option. A new editpane (which is created by split actions)
> seemed to be configured.
>
> Could you please check that the value is applied to existing gutters?

Fixed in r14978.

> And one more thing. Please add a note about this new feature in
> CHANGES.txt. Doing it in the same revision with the actual change is
> the best practice.

Also in r14978. The problem is, I often forget to do that.
One thing no less important than this, is the update of the user docs
of jEdit. I don't do that both because I forget, and because I don't
have the infrastructure for building the jEdit docs. If this could
somehow be simplified, it would be great help. In this specific case,
I think the addition of a GUI option should be added to the user docs.

> --
> k_satoda
>