Davide P. Cervone 3d36b7a4ba Make minus in <mn> produce U+2212 rather than U+002D. Resolves issue #989.		2016-06-14 20:00:10 -04:00
..
config.js	Update version numbers of changed files	2016-02-07 15:34:12 -05:00
jax.js	Make minus in <mn> produce U+2212 rather than U+002D. Resolves issue #989.	2016-06-14 20:00:10 -04:00