diff --git a/frontend/editor.css b/frontend/editor.css index fb756026d4..46a8c2c347 100644 --- a/frontend/editor.css +++ b/frontend/editor.css @@ -3464,8 +3464,6 @@ pluto-cell.code_differs .cm-editor .cm-gutters { position: absolute; right: 3px; pointer-events: none; - font-family: Arial; - transform: scale(1.8); } .cm-editor .cm-lineNumbers .cm-gutterElement:hover { color: var(--cm-color-line-numbers); diff --git a/frontend/fonts/juliamono.css b/frontend/fonts/juliamono.css index 85af525edd..cd3d10d465 100644 --- a/frontend/fonts/juliamono.css +++ b/frontend/fonts/juliamono.css @@ -1,3 +1,19 @@ +@font-face { + font-family: JuliaMono; + src: url("https://cdn.jsdelivr.net/gh/cormullion/juliamono@0.047/webfonts/JuliaMono-RegularLatin.woff2") format("woff2"); + font-display: swap; + font-weight: 400; + unicode-range: U+00-7F; /* Basic Latin characters */ +} + +@font-face { + font-family: JuliaMono; + src: url("https://cdn.jsdelivr.net/gh/cormullion/juliamono@0.047/webfonts/JuliaMono-BoldLatin.woff2") format("woff2"); + font-display: swap; + font-weight: 700; + unicode-range: U+00-7F; /* Basic Latin characters */ +} + @font-face { font-family: JuliaMono; src: url("https://cdn.jsdelivr.net/gh/cormullion/juliamono@0.047/webfonts/JuliaMono-Regular.woff2") format("woff2");