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