changeset 64872 | 9c194386db8d |
parent 64738 | bcdecd466cb2 |
child 64890 | d8ccbd5305bf |
--- a/src/Pure/build-jars Wed Jan 11 14:48:07 2017 +0100 +++ b/src/Pure/build-jars Wed Jan 11 16:01:19 2017 +0100 @@ -163,6 +163,7 @@ ../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 )