# HG changeset patch # User Thomas Lindae # 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 _ => ""