# HG changeset patch
# User wenzelm
# Date 1647002653 -3600
# Node ID 72112cf37bf7afa5aa3ee5fdb573f18704f290f4
# Parent  481665cc17e6015859e92e147c2f533641941526
tuned;

diff -r 481665cc17e6 -r 72112cf37bf7 src/Tools/VSCode/extension/src/output_view.ts
--- a/src/Tools/VSCode/extension/src/output_view.ts	Fri Mar 11 13:31:46 2022 +0100
+++ b/src/Tools/VSCode/extension/src/output_view.ts	Fri Mar 11 13:44:13 2022 +0100
@@ -99,13 +99,12 @@
 
 function _get_decorations(): string
 {
-  let style: string = ''
+  let style: string[] = []
   for (const key of text_colors) {
-  style += `body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`
-  style += `body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`
+    style.push(`body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`)
+    style.push(`body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`)
   }
-
-  return style
+  return style.join("")
 }
 
 export { Output_View_Provider, get_webview_html, open_webview_link }