author | Thomas Lindae <thomas.lindae@in.tum.de> |
Fri, 05 Jul 2024 13:16:47 +0200 | |
changeset 81072 | d1beb91bf46d |
parent 81071 | e1bfcc2a2c05 |
child 81073 | 2ab384664ac5 |
src/Tools/VSCode/src/component_vscode_extension.scala | file | annotate | diff | comparison | revisions |
--- 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 _ => ""