--- 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
}