ui: allow font customization

This commit is contained in:
undefined committed 2022-02-22 00:24:50 +08:00
1 parent cf1195a6ee
commit 9b2c36efbf
13 files changed
+93 -31

No files matched your search

@@ -231,8 +231,6 @@ const page = new NamedPage(['problem_detail', 'contest_detail_problem', 'homewor
{ value: UiContext.pdoc.stats.WA, name: 'WA' },
{ value: UiContext.pdoc.stats.RE, name: 'RE' },
{ value: UiContext.pdoc.stats.CE, name: 'CE' },
{ value: UiContext.pdoc.stats.SE, name: 'SE' },
{ value: UiContext.pdoc.stats.IGN, name: 'IGN' },
],
},
],