From 4920cb092c3dcbfb380fb09ea8dc5afc3d45d918 Mon Sep 17 00:00:00 2001
From: Christopher Haster <geky@geky.net>
Date: Sun, 12 May 2024 23:48:49 -0500
Subject: [PATCH] Fixed summary.py's float diff rendering precision

The internal Float type was incorrectly inheriting the diff rendering
from Int, which casts to, well, an int.
---
 scripts/summary.py | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/scripts/summary.py b/scripts/summary.py
index 608081a0..301245cc 100755
--- a/scripts/summary.py
+++ b/scripts/summary.py
@@ -157,7 +157,18 @@ class Float(co.namedtuple('Float', 'x')):
     table = Int.table
     diff_none = Int.diff_none
     diff_table = Int.diff_table
-    diff_diff = Int.diff_diff
+
+    def diff_diff(self, other):
+        new = self.x if self else 0
+        old = other.x if other else 0
+        diff = new - old
+        if diff == +m.inf:
+            return '%7s' % '+∞'
+        elif diff == -m.inf:
+            return '%7s' % '-∞'
+        else:
+            return '%+7.1f' % diff
+
     ratio = Int.ratio
     __add__ = Int.__add__
     __sub__ = Int.__sub__