tuned signature;
authorwenzelm
Sun, 06 Mar 2022 15:47:09 +0100
changeset 75229 075467e070ba
parent 75228 33fb3014876f
child 75230 bbbee54b1198
tuned signature;
src/Pure/Admin/build_jedit.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/Admin/build_jedit.scala	Sat Mar 05 21:52:21 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Sun Mar 06 15:47:09 2022 +0100
@@ -470,9 +470,10 @@
 """)
 
 
-    /* diff */
+    /* make patch */
 
-    Isabelle_System.make_patch(component_dir, Path.basic(jedit), Path.basic(jedit_patched))
+    File.write(component_dir + Path.basic(jedit).patch,
+      Isabelle_System.make_patch(component_dir, Path.basic(jedit), Path.basic(jedit_patched)))
 
     if (!original) Isabelle_System.rm_tree(jedit_dir)
 
--- a/src/Pure/System/isabelle_system.scala	Sat Mar 05 21:52:21 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Mar 06 15:47:09 2022 +0100
@@ -437,13 +437,15 @@
     else error("Expected to find GNU tar executable")
   }
 
-  def make_patch(base_dir: Path, src: Path, dst: Path, target_dir: Path = Path.current): Path =
+  def make_patch(base_dir: Path, src: Path, dst: Path): String =
   {
-    val target = target_dir + src.base.patch
-    Isabelle_System.bash(
-      "diff -ru " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(target),
-      cwd = base_dir.file).check_rc(_ <= 1)
-    (base_dir + target).expand
+    with_tmp_file("patch")(patch =>
+    {
+      Isabelle_System.bash(
+        "diff -ru " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch),
+        cwd = base_dir.file).check_rc(_ <= 1)
+      File.read(patch)
+    })
   }
 
   def hostname(): String = bash("hostname -s").check.out