Join GitHub today
GitHub is home to over 36 million developers working together to host and review code, manage projects, and build software together.Sign up
Stretched delimiter clipped in HTML-CSS output #701
The output of
has a stretched bracket that is clipped at the top and bottom in HTML-CSS output. It may be that the height and depth aren't being adjusted to accommodate the larger size of the stretched delimiter, when it stretched beyond the required size.
Indeed, the problem was that the row didn't grow when a stretchy operator uses one of the fixed-size versions that is bigger than the height requested. The size of the row probably should be increased to accommodate the larger operator, but that would mean that other rows might need to be modified (e.g., if
Instead, for now I've allowed the stretched operator to extend beyond the height or depth of the row. This means it could overlap neighboring rows (or if the top and bottom, it could extend outside the table). We may need a better solution in the future.