equal
deleted
inserted
replaced
24 "editor.renderIndentGuides": false, |
24 "editor.renderIndentGuides": false, |
25 "editor.rulers": [80, 100], |
25 "editor.rulers": [80, 100], |
26 "editor.unicodeHighlight.ambiguousCharacters": false, |
26 "editor.unicodeHighlight.ambiguousCharacters": false, |
27 "extensions.autoCheckUpdates": false, |
27 "extensions.autoCheckUpdates": false, |
28 "extensions.autoUpdate": false, |
28 "extensions.autoUpdate": false, |
29 "files.encoding": "utf8isabelle", |
|
30 "terminal.integrated.fontFamily": "monospace", |
29 "terminal.integrated.fontFamily": "monospace", |
31 "update.mode": "none" |
30 "update.mode": "none" |
32 } |
31 } |
33 """ |
32 """ |
34 |
33 |