From ef570256e928edc7387ee862789f32f85060b4cd Mon Sep 17 00:00:00 2001
From: Paul Berg <paul@plutojl.org>
Date: Mon, 14 Oct 2024 14:31:18 +0200
Subject: [PATCH] docs: use JuliaMono (#3057)

Co-authored-by: Fons van der Plas <fonsvdplas@gmail.com>
---
 frontend/editor.css | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/frontend/editor.css b/frontend/editor.css
index fdaff31f2..dac3fc711 100644
--- a/frontend/editor.css
+++ b/frontend/editor.css
@@ -2551,7 +2551,8 @@ body > pluto-helpbox > header > button:is(.helpbox-close, .helpbox-popout) {
 .helpbox-docs code,
 .helpbox-docs .cm-line {
     /* from https://docs.julialang.org/en/v1/assets/themes/documenter-light.css */
-    font-family: "Roboto Mono", "SFMono-Regular", "Menlo", "Consolas", "Liberation Mono", "DejaVu Sans Mono", monospace;
+    font-family: var(--julia-mono-font-stack);
+    font-variant-ligatures: none;
     font-size: 0.95em;
     line-height: initial;
 }