From e973a5e965d72c4d8073583578c2169caa5c1530 Mon Sep 17 00:00:00 2001
From: Bzly <clampstand@gmail.com>
Date: Fri, 24 Nov 2017 00:01:55 +0000
Subject: [PATCH] Properly fix monospace on Windows bug

The actual issue (workaround committed in #119) was that font-family names should _not_ be quoted.
---
 src/static/commandline.css | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/static/commandline.css b/src/static/commandline.css
index 32388d5f..fcf0b7f4 100644
--- a/src/static/commandline.css
+++ b/src/static/commandline.css
@@ -6,8 +6,7 @@ body {
 input {
   width: 100%;
   padding: 0;
-  /* MS doesn't know what monospace is */
-  font-family: "monospace", "Courier New";
+  font-family: monospace;
   font-size: 9pt;
   line-height: 1.5;
   color: black;
@@ -25,8 +24,7 @@ input {
   color: black;
   display: inline-block;
   font-size: 10pt;
-  /* MS doesn't know what monospace is */
-  font-family: "monospace", "Courier New";
+  font-family: monospace;
   overflow: hidden;
   width: 100%;
   border-top: 0.5px solid grey;