avoid whitespace if none needed

This commit is contained in:
Hannes Mehnert 2024-03-14 21:22:14 +01:00
parent 745e816cc2
commit 056c76536e

View file

@ -102,6 +102,7 @@ let pp ?(row_numbers = true) ?(chars = true) () ppf s =
String.sub s (l - (l mod 16)) (l mod 16), String.sub s (l - (l mod 16)) (l mod 16),
pad pad
in in
if pad > 0 then
let pad_chars = pad * 2 + (pad + 1) / 2 + (if pad > 8 then 1 else 0) + 1 in let pad_chars = pad * 2 + (pad + 1) / 2 + (if pad > 8 then 1 else 0) + 1 in
Format.pp_print_string ppf (String.make pad_chars ' '); Format.pp_print_string ppf (String.make pad_chars ' ');
String.iter (fun c -> String.iter (fun c ->