| changeset 82654 | 60bd591ef3fc |
| parent 81297 | 07f64697408e |
| 82647:21c3b55787a6 | 82654:60bd591ef3fc |
|---|---|
10 + setFonts(); |
10 + setFonts(); |
11 + } |
11 + } |
12 |
12 |
13 // This is handled a little differently from other jEdit settings |
13 // This is handled a little differently from other jEdit settings |
14 // as this flag needs to be known very early in the |
14 // as this flag needs to be known very early in the |
15 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java |