# HG changeset patch # User wenzelm # Date 1737064096 -3600 # Node ID 7c92343b5408ab680cf53d4ad5376d7a7a2350db # Parent 4bb6c49ef791cb69f69c47fd528ceb13cb20950f more robust options; more robust lines; diff -r 4bb6c49ef791 -r 7c92343b5408 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Jan 16 13:14:24 2025 +0100 +++ b/src/Pure/System/isabelle_system.scala Thu Jan 16 22:48:16 2025 +0100 @@ -494,13 +494,12 @@ } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { - with_tmp_file("patch") { patch => + val lines = Isabelle_System.bash( - "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + - " > " + File.bash_path(patch), - cwd = base_dir).check_rc(_ <= 1) - File.read(patch) - } + "diff -Nru" + if_proper(diff_options, " " + diff_options) + " -- " + + File.bash_path(src) + " " + File.bash_path(dst), + cwd = base_dir).check_rc(Process_Result.RC.regular).out_lines + Library.terminate_lines(lines) } def git_clone(url: String, target: Path, diff -r 4bb6c49ef791 -r 7c92343b5408 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Thu Jan 16 13:14:24 2025 +0100 +++ b/src/Pure/System/process_result.scala Thu Jan 16 22:48:16 2025 +0100 @@ -18,6 +18,8 @@ val interrupt = 130 val timeout = 142 + val regular: Set[Int] = Set(ok, error) + private def text(rc: Int): String = { val txt = rc match {