tuned;
authorwenzelm
Fri, 11 Mar 2022 13:44:13 +0100
changeset 75266 72112cf37bf7
parent 75265 481665cc17e6
child 75267 6369151119ee
tuned;
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 }