--- 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"))
})