changeset 72212 | 53e8858b839f |
parent 72136 | 98dca728fc9c |
child 72322 | 9bb16dcb9ed8 |
--- a/src/Pure/Tools/build.scala Wed Aug 26 15:59:21 2020 +0100 +++ b/src/Pure/Tools/build.scala Thu Aug 27 12:34:10 2020 +0200 @@ -308,7 +308,7 @@ if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") } yield props1.filter(p => Markup.command_timing_properties(p._1)) - val functions = + override val functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory,