# HG changeset patch # User wenzelm # Date 1735999403 -3600 # Node ID f6c82d6ff8620e18bd3f2980e6a19845df59aab9 # Parent 04f87dbd0e97b6c8e0fff0969a94c4253e2b0fec unused; diff -r 04f87dbd0e97 -r f6c82d6ff862 src/Pure/Admin/component_e.scala --- a/src/Pure/Admin/component_e.scala Sat Jan 04 12:51:59 2025 +0100 +++ b/src/Pure/Admin/component_e.scala Sat Jan 04 15:03:23 2025 +0100 @@ -19,8 +19,6 @@ progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { - Isabelle_System.require_command("patch") - Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */