A Nix-friendly SQLite-enhanced fork of Flitter, a speedrunning split timer for Unix-style terminals
Revision | 2fffe4624a7a0ee6d17ffc197e77a17fa3608ccf (tree) |
---|---|
Zeit | 2020-08-20 10:08:26 |
Autor | Alex Morson <alexmorson@btin...> |
Commiter | Alex Morson |
Fix millisecond padding bug
Milliseconds were being zero padded in the wrong direction, meaning that
a time of eg. 24.017 would be displayed as 24.170
@@ -24,11 +24,6 @@ let left_pad_zeros size str = | ||
24 | 24 | left_pad_zeros_char_list str size |
25 | 25 | |> String.of_char_list |
26 | 26 | |
27 | -let right_pad_zeros size str = | |
28 | - left_pad_zeros_char_list str size | |
29 | - |> List.rev | |
30 | - |> String.of_char_list | |
31 | - | |
32 | 27 | let of_string str = |
33 | 28 | match Re.exec_opt compiled_re str with |
34 | 29 | | None -> None |
@@ -41,7 +36,7 @@ let of_string str = | ||
41 | 36 | let hours = group_strs.(2) |> to_int_default in |
42 | 37 | let minutes = group_strs.(3) |> to_int_default in |
43 | 38 | let seconds = group_strs.(4) |> to_int_default in |
44 | - let millis = group_strs.(5) |> right_pad_zeros 3 |> to_int_default in | |
39 | + let millis = group_strs.(5) |> left_pad_zeros 3 |> to_int_default in | |
45 | 40 | |
46 | 41 | Some ( |
47 | 42 | day * days + |