fix: binom delimiter size in scriptscriptstyle. (#2976)

Co-authored-by: Erik Demaine <edemaine@mit.edu>
This commit is contained in:
Ron Kok
2021-05-06 11:27:10 -07:00
committed by GitHub
parent 9cc58a8c08
commit 980b004023
6 changed files with 3 additions and 1 deletions

View File

@@ -152,6 +152,8 @@ const htmlBuilder = (group, options) => {
let delimSize;
if (style.size === Style.DISPLAY.size) {
delimSize = options.fontMetrics().delim1;
} else if (style.size === Style.SCRIPTSCRIPT.size) {
delimSize = options.havingStyle(Style.SCRIPT).fontMetrics().delim2;
} else {
delimSize = options.fontMetrics().delim2;
}