# HG changeset patch
# User wenzelm
# Date 1713981925 -7200
# Node ID 273a8fa8a44ea50aa6bd70c0977a4b0d32aa9b09
# Parent  8e3730b527e98e22c52bcbeda6a7a3f0a1c23f78
more robust;

diff -r 8e3730b527e9 -r 273a8fa8a44e src/Pure/Admin/component_e.scala
--- a/src/Pure/Admin/component_e.scala	Wed Apr 24 19:48:45 2024 +0200
+++ b/src/Pure/Admin/component_e.scala	Wed Apr 24 20:05:25 2024 +0200
@@ -19,6 +19,8 @@
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
+    Isabelle_System.require_command("patch")
+
     Isabelle_System.with_tmp_dir("build") { tmp_dir =>
       /* component */