tools/sizes.py: Change Unicode box-drawing chars to that of double ve…

…rsion (#8573)

Due to historical circumstances, some of light/heavy version of Unicode
box-drawing chars may have twice width of others (aka. "Zen-Kaku" in Japanese,
means full-square), eg. All of '─'(U+2500), '│'(U+2502), '└'(U+2514) and
'├'(U+251C) correspond to that in Windows Japanese fonts and locale.

Double versions, '═'(U+2550), '║'(U+2551), '╚'(U+255A) and '╠'(U+2560) are
not like that.

(See [Box Drawing, The Unicode Standard](https://www.unicode.org/charts/PDF/U2500.pdf))

tools/sizes.py

@@ -110,9 +110,9 @@ def safe_prefix(n, length):
 
 def prefix(n, length):
     if n == length:
-        return "└──"
+        return "╚══"
 
-    return "├──"
+    return "╠══"
 
 
 def filter_segments(segments):
@@ -159,7 +159,10 @@ def main():
         number, used, segments = filter_segments(segments)
 
         print(f". {group:<8}, used {used} / {total} bytes ({percentage(used, total)})")
-        print("|   SEGMENT  BYTES    DESCRIPTION")
+        try:
+            print("║   SEGMENT  BYTES    DESCRIPTION")
+        except UnicodeEncodeError:
+            print("|   SEGMENT  BYTES    DESCRIPTION")
         for n, segment, size in segments:
             try:
                 print(f"{prefix(n, number)} ", end="")