src/Pure/build-jars
changeset 68758 a110e7e24e55
parent 68713 fb44580680c4
child 68845 3b2daa7bf9f4
--- a/src/Pure/build-jars	Fri Aug 17 21:34:56 2018 +0200
+++ b/src/Pure/build-jars	Sat Aug 18 12:41:05 2018 +0200
@@ -93,6 +93,7 @@
   PIDE/command_span.scala
   PIDE/document.scala
   PIDE/document_id.scala
+  PIDE/document_status.scala
   PIDE/editor.scala
   PIDE/line.scala
   PIDE/markup.scala