From 903523f5153ad92d9eaa9e1cb21939e6759fbac4 Mon Sep 17 00:00:00 2001 From: omriisack <39183763+omriisack@users.noreply.github.com> Date: Tue, 3 Dec 2024 12:17:14 +0200 Subject: [PATCH] Minor --- src/common/Statistics.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/common/Statistics.cpp b/src/common/Statistics.cpp index f7efa15e7..b9f7e72e5 100644 --- a/src/common/Statistics.cpp +++ b/src/common/Statistics.cpp @@ -427,8 +427,7 @@ void Statistics::print() getUnsignedAttribute( Statistics::NUM_CERTIFIED_LEAVES ) ); printf( "\tNumber of leaves to delegate: %u\n", getUnsignedAttribute( Statistics::NUM_DELEGATED_LEAVES ) ); - printf( "\tNumber of lemmas: %u\n", - getUnsignedAttribute( Statistics::NUM_LEMMAS ) ); + printf( "\tNumber of lemmas: %u\n", getUnsignedAttribute( Statistics::NUM_LEMMAS ) ); } unsigned long long Statistics::getTotalTimeInMicro() const