diff options
| author | Emilio Jesus Gallego Arias | 2016-12-04 11:40:36 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-12-04 22:57:51 +0100 |
| commit | ac9f2b1a5789964b1d881d024912350a7506a0f9 (patch) | |
| tree | 5d9d6a9ded48c3505150f4977b1b8c1f1f924023 /kernel/nativecode.ml | |
| parent | f653036a73f008168809d3f50041382fe3ee52a1 (diff) | |
[pp] Set printing width for richpp formatter (bug #5244)
Richpp output depends on printing width, thus its internal formatter
should be seeded with the proper width value.
While we are at it, we increase the default buffer size to a more
sensible value.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions