diff options
| author | Hugo Herbelin | 2015-05-20 14:47:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-20 22:48:06 +0200 |
| commit | 8241460f5a729b577b0d7da544fe8f8fcda18d14 (patch) | |
| tree | 1f366937bf868551b49bb2d0a711c071c612ac01 /kernel/nativecode.ml | |
| parent | 69941d4e195650bf59285b897c14d6287defea0f (diff) | |
Answering report #4241 (formatting of boxes not behaving regularly
when printing width extend).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions