author | wenzelm |
Wed, 02 Mar 2022 15:28:02 +0100 | |
changeset 75178 | 01017b938135 |
parent 75177 | 74f0110bbd0a |
child 75179 | 549e4fb76724 |
child 75180 | 75695a504822 |
--- 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" } """