Revert "use noto emoji font"

This reverts commit 9a1d0f3.
leanprover-community · May 14, 2024 · f7ee513 · f7ee513
1 parent 9a1d0f3
commit f7ee513
Show file tree

Hide file tree

Showing 4 changed files with 1 addition and 99 deletions.
diff --git a/client/public/fonts/LICENSE-NotoColorEmoji b/client/public/fonts/LICENSE-NotoColorEmoji
diff --git a/client/public/fonts/NotoColorEmoji-Regular.ttf b/client/public/fonts/NotoColorEmoji-Regular.ttf
diff --git a/client/src/css/index.css b/client/src/css/index.css
@@ -13,8 +13,3 @@ body {
   font-family: 'JuliaMono';
   src: local('JuliaMono'), url('/fonts/JuliaMono-Regular.ttf') format('truetype');
 }
-
-@font-face {
-  font-family: 'NotoColorEmoji';
-  src: local('NotoColorEmoji'), url('/fonts/NotoColorEmoji-Regular.ttf') format('truetype');
-}
diff --git a/client/src/editor/vscode.css b/client/src/editor/vscode.css
@@ -1,7 +1,7 @@
 :root {
   --vscode-font-weight:normal;
   --vscode-font-size:13px;
-  --vscode-editor-font-family: 'NotoColorEmoji', 'JuliaMono', 'Source Code Pro', 'STIX Two Math', monospace;
+  --vscode-editor-font-family: 'JuliaMono', 'Source Code Pro', 'STIX Two Math', monospace;
   --vscode-editor-font-weight:normal;
   --vscode-editor-font-size:15px;
   --vscode-foreground: #616161;