src/Pure/Build/build_job.scala
changeset 83313 73abc1020bfd
parent 83312 6b4028763591
child 83315 03dfb684a50d
--- 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
     }