diff options
| author | Gaëtan Gilbert | 2019-07-05 09:16:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-05 11:55:10 +0200 |
| commit | 115785b3678ef333cd5db2447f832abc7a64a8b1 (patch) | |
| tree | 27c8c5cec9641c00d9950da703e4655778194e6c /plugins | |
| parent | 37d417f664fc14e14bbcf09d479c4bffbe5ee178 (diff) | |
Use Format.pp_print_list with conditional instead of fold for list prints in gramlib
This means we don't need to ignore the result of the fold. cf #10471
Using Format.pp_print_list instead of a custom iteri was suggested by
Jean-Christophe Léchenet (eponier)
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions