--- a/src/Pure/build-jars Tue Dec 20 08:53:26 2016 +0100
+++ b/src/Pure/build-jars Tue Dec 20 08:57:03 2016 +0100
@@ -86,6 +86,7 @@
PIDE/document.scala
PIDE/document_id.scala
PIDE/editor.scala
+ PIDE/line.scala
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
@@ -157,7 +158,6 @@
../Tools/Graphview/tree_panel.scala
../Tools/VSCode/src/channel.scala
../Tools/VSCode/src/document_model.scala
- ../Tools/VSCode/src/line.scala
../Tools/VSCode/src/protocol.scala
../Tools/VSCode/src/server.scala
../Tools/VSCode/src/uri_resources.scala