Tweak keyboard font.

2022-08-09 23:41:42 -07:00
parent 5277b6dbbb
commit 356a9204a4
1 changed files with 1 additions and 0 deletions
--- a/web/platform.fs
+++ b/web/platform.fs
@ -298,6 +298,7 @@ if (!globalObj.write) {
      return;
    }
    var k = document.createElement('button');
+    k.style.fontFamily = 'monospace';
    k.style.verticalAlign = 'middle';
    k.style.border = 'none';
    k.style.margin = '0';