--- a/src/Pure/build-jars Tue Mar 07 10:52:04 2017 +0100
+++ b/src/Pure/build-jars Tue Mar 07 13:55:49 2017 +0100
@@ -160,12 +160,12 @@
../Tools/Graphview/popups.scala
../Tools/Graphview/shapes.scala
../Tools/Graphview/tree_panel.scala
+ ../Tools/VSCode/src/build_vscode.scala
../Tools/VSCode/src/channel.scala
../Tools/VSCode/src/document_model.scala
../Tools/VSCode/src/grammar.scala
../Tools/VSCode/src/protocol.scala
../Tools/VSCode/src/server.scala
- ../Tools/VSCode/src/symbols.scala
../Tools/VSCode/src/vscode_rendering.scala
../Tools/VSCode/src/vscode_resources.scala
)