#3814 Caret "thick' options does nothing

normal bug
closed-fixed
Alan Ezust
5
2013-07-26
2013-07-24
Edward Diener
No
0 up votes | 0 down votes | 0%
1 comment

JEdit 5.0, Windows 7 Ultimate, Java 1.7.0_25

There is no documentation about what the caret "thick" option on the Text Area option page is supposed to do, but I am guessing it is supposed to draw a thicker caret. It does not do this or do anything AFAICS.

Discussion

  • Alan Ezust
    Alan Ezust
    2013-07-26

    committed 23077. Opened merge request 3614811 for jedit 5.1

     
  • Alan Ezust
    Alan Ezust
    2013-07-26

    • assigned_to: nobody --> ezust
    • status: open --> closed-fixed