src/Pure/Admin/component_jedit.scala
changeset 80224 db92e0b6a11a
parent 77566 2a99fcb283ee
child 81297 07f64697408e
--- a/src/Pure/Admin/component_jedit.scala	Fri May 31 22:35:44 2024 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Sat Jun 01 12:31:06 2024 +0200
@@ -161,7 +161,7 @@
         if !File.is_backup(name)
       } {
         progress.bash("patch -p2 < " + File.bash_path(File.path(file)),
-          cwd = source_dir.file, echo = true).check
+          cwd = source_dir, echo = true).check
       }
 
       for { theme <- List("classic", "tango") } {
@@ -173,7 +173,7 @@
       progress.echo("Building jEdit ...")
       Isabelle_System.copy_dir(source_dir, tmp_source_dir)
       progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
-        cwd = tmp_source_dir.file, echo = true).check
+        cwd = tmp_source_dir, echo = true).check
       Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
 
       val java_sources =