set font-size in goal-view Message and Goal

coq · Jan 4, 2024 · 997ebcc · 997ebcc
1 parent d4a702e
commit 997ebcc
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%;