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