equal
deleted
inserted
replaced
40 "editor.fontFamily": "'Isabelle DejaVu Sans Mono'", |
40 "editor.fontFamily": "'Isabelle DejaVu Sans Mono'", |
41 "editor.fontSize": 18, |
41 "editor.fontSize": 18, |
42 "editor.lineNumbers": "off", |
42 "editor.lineNumbers": "off", |
43 "editor.renderIndentGuides": false, |
43 "editor.renderIndentGuides": false, |
44 "editor.rulers": [80, 100], |
44 "editor.rulers": [80, 100], |
45 "update.mode": "none" |
45 "update.mode": "none", |
|
46 "extensions.autoCheckUpdates": false, |
|
47 "extensions.autoUpdate": false |
46 } |
48 } |
47 """ |
49 """ |
48 |
50 |
49 |
51 |
50 /* patch resources */ |
52 /* patch resources */ |