From 959218f7a9ee6754ec026b449837300c277a3f7b Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Sat, 15 Feb 2014 16:44:49 -0500
Subject: [PATCH] Adjust positions of extenders for double-lined vertical
 arrows.  (The horizontal position of the extender is off in teh fonts.) 
 Resolves issue #476.

---
 unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js
index 6ee865d4f..1943c6d4c 100644
--- a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js
+++ b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js
@@ -252,7 +252,7 @@
         },
         0x21D1: // \Uparrow
         {
-          dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x21D1,GENERAL], ext:[0x2225,GENERAL,.1]}
+          dir: V, HW: [[.818,GENERAL]], stretch: {top:[0x21D1,GENERAL], ext:[0x2225,GENERAL,.082]}
         },
         0x21D2: // right double arrow
         {
@@ -260,7 +260,7 @@
         },
         0x21D3: // \Downarrow
         {
-          dir: V, HW: [[.818,GENERAL]], stretch: {ext:[0x2225,GENERAL,.1], bot:[0x21D3,GENERAL]}
+          dir: V, HW: [[.818,GENERAL]], stretch: {ext:[0x2225,GENERAL,.082], bot:[0x21D3,GENERAL]}
         },
         0x21D4: // left-right double arrow
         {
@@ -270,7 +270,7 @@
         0x21D5: // \Updownarrow
         {
           dir: V, HW: [[.818,GENERAL]],
-          stretch: {top:[0x21D1,GENERAL], ext:[0x2225,GENERAL,.1], bot:[0x21D3,GENERAL]}
+          stretch: {top:[0x21D1,GENERAL], ext:[0x2225,GENERAL,.082], bot:[0x21D3,GENERAL]}
         },
         0x221A: // \surd
         {