src/Pure/build-jars
changeset 64611 d72d63d05bdb
parent 64610 1b89608974e9
child 64617 01e50039edc9
--- 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