feat: make spinner size scale with font size

leanprover · Nov 8, 2024 · 926f7c1 · 926f7c1
1 parent 2afbbaf
commit 926f7c1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -71,7 +71,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
         transitionProperty: 'opacity',
         transitionTimingFunction: 'ease-in',
         color: 'var(--vscode-editor-foreground)',
-        fontSize: '10px',
+        fontSize: 'calc(0.8 * var(--vscode-font-size))',
     }
 
     return (