tuned;

--- a/src/Pure/build-jars	Thu Nov 22 10:06:31 2018 +0000
+++ b/src/Pure/build-jars	Thu Nov 22 15:47:58 2018 +0100
@@ -139,12 +139,12 @@
   Thy/thy_element.scala
   Thy/thy_header.scala
   Thy/thy_syntax.scala
-  Tools/dump.scala
   Tools/build.scala
   Tools/build_docker.scala
   Tools/check_keywords.scala
   Tools/debugger.scala
   Tools/doc.scala
+  Tools/dump.scala
   Tools/imports.scala
   Tools/main.scala
   Tools/mkroot.scala