diff -r 6b4028763591 -r 73abc1020bfd src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Sat Oct 18 21:20:30 2025 +0200 +++ b/src/Pure/Build/build_job.scala Sun Oct 19 13:36:57 2025 +0200 @@ -122,14 +122,11 @@ } def stop_process_output(): Unit = synchronized { - if (process_output_writer.isDefined) { - process_output_writer.get.close() - process_output_writer = None - } + process_output_writer.foreach(_.close()) + process_output_writer = None } def clean_process_output(): Unit = synchronized { - process_output_writer.foreach(_.close()) process_output_file.delete }