# HG changeset patch
# User wenzelm
# Date 1677681958 -3600
# Node ID 0093124710db8c0b7f1f0017cb150d0147a075a2
# Parent  167b5095ba14100087032395aac88eb9fbdc5e92
unused;

diff -r 167b5095ba14 -r 0093124710db src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 15:43:38 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 15:45:58 2023 +0100
@@ -88,9 +88,6 @@
     val old_time: Time,
     val old_command_timings_blob: Bytes
   ) {
-    def is_empty: Boolean =
-      old_time.is_zero && old_command_timings_blob.is_empty
-
     override def toString: String = name
   }