# HG changeset patch # User wenzelm # Date 1646578029 -3600 # Node ID 075467e070bafd3faa29b30fa957e56c925024e7 # Parent 33fb3014876fe63fb982605f167a332ac6d7ccf4 tuned signature; diff -r 33fb3014876f -r 075467e070ba src/Pure/Admin/build_jedit.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) diff -r 33fb3014876f -r 075467e070ba src/Pure/System/isabelle_system.scala --- 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