# HG changeset patch
# User wenzelm
# Date 1542898078 -3600
# Node ID 600df66ac561be43a76f367ad76e910299d45c6d
# Parent  4b6ddc5989fca8350458c3cb008c2c73647df437
tuned;

diff -r 4b6ddc5989fc -r 600df66ac561 src/Pure/build-jars
--- 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