# 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 {