This commit is contained in:
2025-07-23 08:59:52 +02:00
parent c283155c5a
commit b08c426877
3 changed files with 35 additions and 8 deletions

View File

@@ -81,9 +81,8 @@
html.elem("style", "
@font-face {
font-family: 'DejaVu Sans Mono';
src: url('res/DejaVuSansMono-Bold.woff2') format('woff2'),
url('res/DejaVuSansMono-Bold.woff') format('woff'),
local('DejaVu Sans Mono'),
src:local('DejaVu Sans Mono'),
url('res/DejaVuSansMono-Bold.woff2') format('woff2'),
local('Courier New'),
local(Courier),
local(monospace);
@@ -94,9 +93,8 @@ html.elem("style", "
@font-face {
font-family: 'DejaVu Sans Mono';
src: url('res/DejaVuSansMono.woff2') format('woff2'),
url('res/DejaVuSansMono.woff') format('woff'),
local('DejaVu Sans Mono'),
src:local('DejaVu Sans Mono'),
url('res/DejaVuSansMono.woff2') format('woff2'),
local('Courier New'),
local(Courier),
local(monospace);
@@ -105,6 +103,26 @@ html.elem("style", "
font-display: swap;
}
@font-face {
font-family: 'DejaVu Sans';
src:local('DejaVu Sans'),
url('res/DejaVuSans-Bold.woff2') format('woff2'),
local('Courier New');
font-weight: bold;
font-style: normal;
font-display: swap;
}
@font-face {
font-family: 'DejaVu Sans';
src:local('DejaVu Sans'),
url('res/DejaVuSans.woff2') format('woff2'),
local('Courier New');
font-weight: normal;
font-style: normal;
font-display: swap;
}
body {
font-family: DejaVu Sans Mono;
font-size: "+len2css(default-font-size)+";