Merge pull request #704 from LittleJianCH/main

Fix font-size in Coq Goals
coq · Jan 30, 2024 · b257360 · b257360
2 parents 1ae429c + 997ebcc
commit b257360
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/client/goal-view-ui/src/components/atoms/PpString.module.css b/client/goal-view-ui/src/components/atoms/PpString.module.css
@@ -2,6 +2,7 @@
     margin-top: 12px;
     width: 100%;
     font-family: var(--vscode-editor-font-family);
+    font-size: var(--vscode-editor-font-size);
 }
 
 .Error {
@@ -22,6 +23,7 @@
 
 .Goal {
     font-family: var(--vscode-editor-font-family);
+    font-size: var(--vscode-editor-font-size);
     color: var(--vscode-editor-foreground);
     white-space: pre-wrap;
     width: 100%;