changeset 75178 | 01017b938135 |
parent 75171 | 96b26b0d2cc5 |
child 75202 | 4fdde010086f |
--- a/src/Tools/VSCode/src/vscode_setup.scala Wed Mar 02 15:08:49 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Wed Mar 02 15:28:02 2022 +0100 @@ -84,6 +84,7 @@ "editor.unicodeHighlight.ambiguousCharacters": false, "extensions.autoCheckUpdates": false, "extensions.autoUpdate": false, + "terminal.integrated.fontFamily": "monospace", "update.mode": "none" } """