From 14fd3918eda0615fca0d18ec5a096733de188eb3 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Mon, 8 Sep 2014 15:23:42 -0400
Subject: [PATCH] Use delimitershortfall and delimiterfactor for stretching
 vertical delimiters.  Resolves issue #829.

---
 unpacked/jax/output/HTML-CSS/jax.js | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/unpacked/jax/output/HTML-CSS/jax.js b/unpacked/jax/output/HTML-CSS/jax.js
index 7a5292568..0e325f26e 100644
--- a/unpacked/jax/output/HTML-CSS/jax.js
+++ b/unpacked/jax/output/HTML-CSS/jax.js
@@ -1680,7 +1680,7 @@
       scriptspace:         .1,
       nulldelimiterspace:  .12,
       delimiterfactor:     901,
-      delimitershortfall:   .1,    // originally .3,
+      delimitershortfall:   .3,
 
       min_rule_thickness:  1.25     // in pixels
     },
@@ -2208,6 +2208,8 @@
 	values.maxsize = HTMLCSS.length2em(values.maxsize,mu,span.bbox.h+span.bbox.d);
 	values.minsize = HTMLCSS.length2em(values.minsize,mu,span.bbox.h+span.bbox.d);
 	H = Math.max(values.minsize,Math.min(values.maxsize,H));
+        if (H != values.minsize)
+          {H = [Math.max(H*HTMLCSS.TeX.delimiterfactor/1000,H-HTMLCSS.TeX.delimitershortfall),H]}
 	span = this.HTMLcreateSpan(box); // clear contents and attributes
 	HTMLCSS.createDelimiter(span,this.data.join("").charCodeAt(0),H,scale);
 	if (values.symmetric) {H = (span.bbox.h + span.bbox.d)/2 + axis}