src/Pure/build-jars
changeset 65138 64dfee6bd243
parent 65077 2d6e716c9d6e
child 65139 0a2c0712e432
     1.1 --- a/src/Pure/build-jars	Tue Mar 07 10:52:04 2017 +0100
     1.2 +++ b/src/Pure/build-jars	Tue Mar 07 13:55:49 2017 +0100
     1.3 @@ -160,12 +160,12 @@
     1.4    ../Tools/Graphview/popups.scala
     1.5    ../Tools/Graphview/shapes.scala
     1.6    ../Tools/Graphview/tree_panel.scala
     1.7 +  ../Tools/VSCode/src/build_vscode.scala
     1.8    ../Tools/VSCode/src/channel.scala
     1.9    ../Tools/VSCode/src/document_model.scala
    1.10    ../Tools/VSCode/src/grammar.scala
    1.11    ../Tools/VSCode/src/protocol.scala
    1.12    ../Tools/VSCode/src/server.scala
    1.13 -  ../Tools/VSCode/src/symbols.scala
    1.14    ../Tools/VSCode/src/vscode_rendering.scala
    1.15    ../Tools/VSCode/src/vscode_resources.scala
    1.16  )