From d63ef8330dfea202116bfef525e1ccac20f1fab7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Omar=20Flores=20Ch=C3=A1vez?= Date: Fri, 11 Oct 2019 07:21:13 -0500 Subject: [PATCH] Add `!important` to `code {font-family}` property (#1062) If accepted, this will fix #1061 --- src/theme/css/general.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/theme/css/general.css b/src/theme/css/general.css index b45f90fb..cb295837 100644 --- a/src/theme/css/general.css +++ b/src/theme/css/general.css @@ -16,7 +16,7 @@ body { } code { - font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace; + font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important; font-size: 0.875em; /* please adjust the ace font size accordingly in editor.js */ }