src/Pure/build-jars
changeset 64617 01e50039edc9
parent 64611 d72d63d05bdb
child 64622 529bbb8977c7
--- a/src/Pure/build-jars	Tue Dec 20 10:45:20 2016 +0100
+++ b/src/Pure/build-jars	Tue Dec 20 16:08:02 2016 +0100
@@ -49,6 +49,7 @@
   General/graphics_file.scala
   General/http_server.scala
   General/json.scala
+  General/length.scala
   General/linear_set.scala
   General/logger.scala
   General/long_name.scala