From 072c02f9a3e1767a7b9121ef5217415bbbc8711f Mon Sep 17 00:00:00 2001 From: Oliver Schneider Date: Fri, 6 Oct 2017 17:12:32 +0200 Subject: [PATCH] Use numbers instead of indentations Noone can differentiate between 8 and 9 spaces if they aren't aligned --- miri/bin/miri.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/miri/bin/miri.rs b/miri/bin/miri.rs index d38f63610a0e..6ea1fac605e1 100644 --- a/miri/bin/miri.rs +++ b/miri/bin/miri.rs @@ -193,14 +193,13 @@ fn resource_limits_from_attributes(state: &CompileState) -> miri::ResourceLimits fn init_logger() { let format = |record: &log::LogRecord| { if record.level() == log::LogLevel::Trace { - // prepend spaces to indent the final string + // prepend frame number let indentation = log_settings::settings().indentation; format!( - "{lvl}:{module}:{indent: