diff --git a/report.py b/report.py index aa08eb5049e24271b6fde874e1f7b90dd2944424..fe033624b92b4e34724201d2ab05c2c5d025d261 100755 --- a/report.py +++ b/report.py @@ -77,8 +77,8 @@ def get_results(filename, args): (spills, fills) = val.split(':') result_group['spills'] = int(spills) result_group['fills'] = int(fills) - elif val.isnumeric(): - result_group[name] = int(val) + elif val.replace('.', '').isnumeric(): + result_group[name] = float(val) else: result_group[name] = val