From d4cd52be45ff717ed4db5a195d85a6f1b6271826 Mon Sep 17 00:00:00 2001 From: Fons van der Plas Date: Wed, 2 Oct 2024 09:57:44 +0200 Subject: [PATCH] Revert "Remove JuliaMono Latin subsets, fix #3029" This reverts commit a1138121415cea5338157b60f41ce860b40bde1d. --- frontend/editor.css | 2 -- frontend/fonts/juliamono.css | 16 ++++++++++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) 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");