author | Oleksandr Gavenko <gavenkoa@gmail.com> |
Tue, 27 Dec 2022 16:14:46 +0200 | |
changeset 1013 | 781084ef85ce |
parent 914 | 0dba496629c9 |
permissions | -rw-r--r-- |
914
0dba496629c9
Allow to override font size by local settings.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff
changeset
|
1 |
# 7x13 on low DPI, 7x14 on hi DPI. |
0dba496629c9
Allow to override font size by local settings.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff
changeset
|
2 |
CFG_FONT_NAME := 7x14 |
0dba496629c9
Allow to override font size by local settings.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff
changeset
|
3 |
# 10 on low DPI, 12 on hi DPI. |
0dba496629c9
Allow to override font size by local settings.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff
changeset
|
4 |
CFG_FONT_SIZE := 12 |
0dba496629c9
Allow to override font size by local settings.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff
changeset
|
5 |
CFG_COLS := 160 |
0dba496629c9
Allow to override font size by local settings.
Oleksandr Gavenko <gavenkoa@gmail.com>
parents:
diff
changeset
|
6 |
CFG_ROWS := 40 |