From 227a67cf8b67450780c1ff43e86ec2a9aa58e9a6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 16 Jun 2021 15:39:01 +0200 Subject: [PATCH] chore: show (first) declaration name with compilation times --- src/library/compiler/compiler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index fcb2fbe5d0..40adefd273 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -187,7 +187,7 @@ environment compile(environment const & env, options const & opts, names cs) { if (!cinfo.is_definition() && !cinfo.is_opaque()) return env; } - time_task t("compilation", opts); + time_task t("compilation", opts, head(cs)); scope_trace_env scope_trace(env, opts); comp_decls ds = to_comp_decls(env, cs);