author | wenzelm |
Wed, 20 Jan 2021 22:55:22 +0100 | |
changeset 73168 | 6d37836c4329 |
parent 73167 | 490ca65ecae2 |
child 73169 | 2ac5a4957f9c |
--- a/src/Tools/VSCode/extension/src/symbol.ts Wed Jan 20 22:43:58 2021 +0100 +++ b/src/Tools/VSCode/extension/src/symbol.ts Wed Jan 20 22:55:22 2021 +0100 @@ -122,7 +122,7 @@ if (prettify_symbols_mode) { prettify_symbols_mode.activate().then(() => { - const substitutions = [] as [Substitution] + const substitutions: Substitution[] = [] for (const entry of names) { const sym = entry[0] substitutions.push(