# HG changeset patch
# User wenzelm
# Date 1646475329 -3600
# Node ID ea65e18c5614c86d7cf4d5882de9c090abb8e157
# Parent  1cbdf9cfc94b6299b1bbc739233cb3f8288e7027
tuned output;

diff -r 1cbdf9cfc94b -r ea65e18c5614 src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Sat Mar 05 11:12:26 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Sat Mar 05 11:15:29 2022 +0100
@@ -191,13 +191,13 @@
           file <- File.find_files(org_source_dir.file, file => file.getName.endsWith(".java"))
           package_name <- Scala_Project.package_name(File.path(file))
           if !exclude_package(package_name)
-        } yield File.path(component_dir.java_path.relativize(file.toPath).toFile)
+        } yield File.path(component_dir.java_path.relativize(file.toPath).toFile).implode
 
       File.write(etc_dir + Path.explode("build.props"),
         "module = " + jedit_patched + "/jedit.jar\n" +
         "no_build = true\n" +
         "requirements = env:JEDIT_JARS\n" +
-        ("sources =" :: java_sources.map(p => "  " + p.implode)).mkString("", " \\\n", "\n"))
+        ("sources =" :: java_sources.sorted.map("  " + _)).mkString("", " \\\n", "\n"))
     })