vscode: changed vscode_unicode_symbols_edits option default to true;
authorThomas Lindae <thomas.lindae@in.tum.de>
Fri, 05 Jul 2024 13:16:47 +0200
changeset 81072 d1beb91bf46d
parent 81071 e1bfcc2a2c05
child 81073 2ab384664ac5
vscode: changed vscode_unicode_symbols_edits option default to true;
src/Tools/VSCode/src/component_vscode_extension.scala
--- a/src/Tools/VSCode/src/component_vscode_extension.scala	Fri Jul 05 13:15:50 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala	Fri Jul 05 13:16:47 2024 +0200
@@ -161,7 +161,7 @@
 
       val default = opt.name match {
         case "vscode_unicode_symbols_output" => "true"
-        case "vscode_unicode_symbols_edits" => "false"
+        case "vscode_unicode_symbols_edits" => "true"
         case "vscode_pide_extensions" => "true"
         case "vscode_html_output" => "true"
         case _ => ""