Update devcontainer.json to enable cdot by default (#6530)

This commit is contained in:
Amaury Chamayou 2024-10-07 13:00:07 +01:00 коммит произвёл GitHub
Родитель afd37ec3fe
Коммит 874c3d4726
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: B5690EEEBB952194
1 изменённых файлов: 1 добавлений и 1 удалений

Просмотреть файл

@ -8,7 +8,7 @@
],
"settings": {
"tlaplus.tlc.statisticsSharing": "share",
"tlaplus.java.options": "-XX:+UseParallelGC",
"tlaplus.java.options": "-XX:+UseParallelGC -Dtlc2.tool.impl.Tool.cdot=true",
"tlaplus.java.home": "/home/codespace/java/current/",
"[tlaplus]": {
"editor.codeActionsOnSave": {