Fix division by zero.

Instead of first dividing by zero and then cleaning up the mess,
simply test whether we're going to divide by zero and do the
right thing based on that test.

diff --git a/source/base/timer.cc b/source/base/timer.cc
index f5680f43ffcfb6bfd8b50ddb7fd0825921eb75d1..1e187d6bc5144e408758a2efbbf1517b325244dd 100644 (file)
--- a/source/base/timer.cc
+++ b/source/base/timer.cc
@@ -506,10 +506,10 @@ TimerOutput::print_summary () const
           out_stream << i->second.total_cpu_time << "s |";
           out_stream << std::setw(10);
           out_stream << std::setprecision(2);
-          double value = i->second.total_cpu_time/total_cpu_time * 100;
-          if (!numbers::is_finite(value))
-            value = 0.0;
-          out_stream << value << "% |";
+          if (total_cpu_time != 0)
+            out_stream << i->second.total_cpu_time/total_cpu_time * 100 << "% |";
+          else
+            out_stream << 0.0 << "% |";
         }
       out_stream << std::endl
                  << "+---------------------------------+-----------+"