From 42f305304bafe1e01580348b7c8f9e6c6d2dd79a Mon Sep 17 00:00:00 2001
From: Ron Kok <ronkok@comcast.net>
Date: Wed, 9 May 2018 06:27:30 -0700
Subject: [PATCH] Fix extensible arrow sup vertical alignment (#1256)

* Fix extensible arrow sup vertical alignment

Fixes issue #1254

* Fix lint error

* Allow small depth
---
 src/buildHTML.js | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/buildHTML.js b/src/buildHTML.js
index ada2ec0e..20969028 100644
--- a/src/buildHTML.js
+++ b/src/buildHTML.js
@@ -532,10 +532,10 @@ export const groupTypes = {
         const arrowShift = -options.fontMetrics().axisHeight +
             0.5 * arrowBody.height;
         // 2 mu kern. Ref: amsmath.dtx: #7\if0#2\else\mkern#2mu\fi
-        let upperShift =
-            -options.fontMetrics().axisHeight - 0.5 * arrowBody.height - 0.111;
-        if (group.value.label === "\\xleftequilibrium") {
-            upperShift -= upperGroup.depth;
+        let upperShift = -options.fontMetrics().axisHeight
+            - 0.5 * arrowBody.height - 0.111; // 0.111 em = 2 mu
+        if (upperGroup.depth > 0.25 || group.value.label === "\\xleftequilibrium") {
+            upperShift -= upperGroup.depth;  // shift up if depth encroaches
         }
 
         // Generate the vlist