# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1720178207 -7200
# Node ID d1beb91bf46da069b18163e178afbaac9310be63
# Parent  e1bfcc2a2c05e8d3b902f223953248fd48d0c82e
vscode: changed vscode_unicode_symbols_edits option default to true;

diff -r e1bfcc2a2c05 -r d1beb91bf46d 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 _ => ""