From 35bd8e0acddd20d65de0e6c7614a7b89f4413124 Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Sat, 14 Mar 2015 18:15:45 -0400 Subject: [PATCH] Better positioning of extender in vertical stretchy delimiters. --- unpacked/jax/output/CommonHTML/jax.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js index e8457cdd0..832f22c81 100644 --- a/unpacked/jax/output/CommonHTML/jax.js +++ b/unpacked/jax/output/CommonHTML/jax.js @@ -767,10 +767,10 @@ var n = Math.ceil((H-h)/(k*(ebox.h+ebox.d)*.9)); H = .9*n*k*(ebox.h+ebox.d) + h; } - var s = 1.1*(H - h)/k + .2*k; // space to cover by extender + var s = 1.1*(H - h)/k + .3; // space to cover by extender s /= (ebox.h+ebox.d); // scale factor; this.Transform(ext, - "translateY("+CHTML.Em(-ebox.d+.05)+") scaleY("+s.toFixed(3).replace(/0+$/,"")+")", + "translateY("+CHTML.Em(-ebox.d+.25)+") scaleY("+s.toFixed(3).replace(/0+$/,"")+")", "left "+CHTML.Em(ebox.d) ); ext.style.paddingTop=ext.style.paddingBottom = 0;