diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-10 10:53:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-29 19:14:07 +0200 |
| commit | e3a7caa0fb44f7a12248a140528462853810a614 (patch) | |
| tree | 6b8efab5834d07308ecd5b2cc19a810d13c376a1 /toplevel | |
| parent | d46dd57462650d1e956d8e80d5aa4e537205de4d (diff) | |
Workaround to fix #7731 (printing not splitting line at break hint).
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions