| Author | DaveJarvis <email> |
|---|---|
| Date | 2020-09-17 21:29:28 GMT-0700 |
| Commit | fe87a147f2ca13b7e02638d719b6612e7218d8dc |
| Parent | 86fd370 |
| } | ||
| } | ||
| - | ||
| - /** | ||
| - * Returns the text editor font size property for handling font size change | ||
| - * events. | ||
| - */ | ||
| - private IntegerProperty fontsSizeProperty() { | ||
| - return UserPreferences.getInstance().fontsSizeEditorProperty(); | ||
| - } | ||
| } | ||
| */ | ||
| p tex { | ||
| - vertical-align: middle; | ||
| + vertical-align: baseline; | ||
| } | ||
| Delta | 1 line added, 9 lines removed, 8-line decrease |
|---|