Make replacement vector arrow stretchy

dpvc · dpvc · commit 01000229f0ee · 2017-07-14T21:34:05.000-04:00
diff --git a/unpacked/jax/output/CommonHTML/fonts/TeX/fontdata.js b/unpacked/jax/output/CommonHTML/fonts/TeX/fontdata.js
@@ -611,7 +611,8 @@
       0x27FB: {alias: 0x21A4, dir:H}, // long left arrow from bar
       0x27FC: {alias: 0x21A6, dir:H}, // long right arrow from bar
       0x27FD: {alias: 0x2906, dir:H}, // long left double arrow from bar
-      0x27FE: {alias: 0x2907, dir:H}  // long right double arrow from bar
+      0x27FE: {alias: 0x2907, dir:H}, // long right double arrow from bar
+      0xE160: {alias: 0x2190, dir:H}, // replacement vector arrow
     }
   };
   

Original file line number	Diff line number	Diff line change
`@@ -611,7 +611,8 @@`
`611`	`611`	`0x27FB: {alias: 0x21A4, dir:H}, // long left arrow from bar`
`612`	`612`	`0x27FC: {alias: 0x21A6, dir:H}, // long right arrow from bar`
`613`	`613`	`0x27FD: {alias: 0x2906, dir:H}, // long left double arrow from bar`
`614`		`- 0x27FE: {alias: 0x2907, dir:H} // long right double arrow from bar`
	`614`	`+ 0x27FE: {alias: 0x2907, dir:H}, // long right double arrow from bar`
	`615`	`+ 0xE160: {alias: 0x2190, dir:H}, // replacement vector arrow`
`615`	`616`	`}`
`616`	`617`	`};`
`617`	`618`