# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1720179007 -7200
# Node ID 2ab384664ac571f64e6be8382b0685961f2b8264
# Parent  d1beb91bf46da069b18163e178afbaac9310be63
vscode: removed unused import;

diff -r d1beb91bf46d -r 2ab384664ac5 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Fri Jul 05 13:16:47 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Jul 05 13:30:07 2024 +0200
@@ -10,7 +10,6 @@
 import * as platform from './platform'
 import * as library from './library'
 import * as file from './file'
-import * as symbol from './symbol'
 import * as vscode_lib from './vscode_lib'
 import * as decorations from './decorations'
 import * as preview_panel from './preview_panel'