diff options
| author | Rodrigo Arias Mallo <rodarima@gmail.com> | 2023-12-09 22:04:02 +0100 |
|---|---|---|
| committer | Rodrigo Arias Mallo <rodarima@gmail.com> | 2024-01-15 19:35:56 +0100 |
| commit | f012e861ff6b8107d64982a09125de5f3eb1c868 (patch) | |
| tree | 8863f135ef194447ba05fb29228f1f748a06d700 /src/tipwin.cc | |
| parent | 8583ace18fe8eda5491341f3ad74b2c9e91d1de5 (diff) | |
Add ui_tab_height option
The default tab height of 16 pixels was causing some usability issues as
the tabs are quite small in large monitors. The default size is
increased to 20 pixels and the new option "ui_tab_height" allows the
user to specify a different value.
Diffstat (limited to 'src/tipwin.cc')
0 files changed, 0 insertions, 0 deletions