From 3e6dd0d5e8b5053c024cc74389ec4def41548eb7 Mon Sep 17 00:00:00 2001 From: Sosuke Suzuki Date: Fri, 18 Sep 2020 03:09:58 +0900 Subject: [PATCH] Use better fonts in Playground (#9193) --- website/static/separate-css/playground.css | 1 + 1 file changed, 1 insertion(+) diff --git a/website/static/separate-css/playground.css b/website/static/separate-css/playground.css index 9202ca067..8507dfb93 100644 --- a/website/static/separate-css/playground.css +++ b/website/static/separate-css/playground.css @@ -144,6 +144,7 @@ header h1 { right: 0; bottom: 0; line-height: 1.6; + font-family: Consolas, Monaco, "Andale Mono", "Ubuntu Mono", monospace; } .bottom-bar {