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; }