docs: use JuliaMono (#3057)

Co-authored-by: Fons van der Plas <[email protected]>
fonsp · Oct 14, 2024 · ef57025 · ef57025
1 parent a288cd1
commit ef57025
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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;
 }