From dc605aa2097f782ce632a110d69b53de09be343d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jonatan=20K=C5=82osko?= <jonatanklosko@gmail.com>
Date: Tue, 4 May 2021 15:48:26 +0200
Subject: [PATCH] Specify editor fallback font

---
 assets/css/utilities.css      | 2 +-
 assets/js/cell/live_editor.js | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/assets/css/utilities.css b/assets/css/utilities.css
index 2d903c608..962864f4c 100644
--- a/assets/css/utilities.css
+++ b/assets/css/utilities.css
@@ -9,6 +9,6 @@
 }
 
 .font-editor {
-  font-family: "JetBrains Mono";
+  font-family: "JetBrains Mono", "Droid Sans Mono", "monospace";
   font-size: 14px;
 }
diff --git a/assets/js/cell/live_editor.js b/assets/js/cell/live_editor.js
index 839d460be..70901d3d6 100644
--- a/assets/js/cell/live_editor.js
+++ b/assets/js/cell/live_editor.js
@@ -102,7 +102,7 @@ class LiveEditor {
       occurrencesHighlight: false,
       renderLineHighlight: "none",
       theme: "custom",
-      fontFamily: "JetBrains Mono",
+      fontFamily: "JetBrains Mono, Droid Sans Mono, monospace",
       tabIndex: -1,
       quickSuggestions: false,
       tabCompletion: "on",