Tue, 21 Jun 2011 22:40:30 +0200 | wenzelm | some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup; | changeset | files |
Tue, 21 Jun 2011 21:34:36 +0200 | wenzelm | more precise font transformations: shift sub/superscript, adjust size for user fonts; | changeset | files |
Tue, 21 Jun 2011 17:17:39 +0200 | blanchet | don't change the way helpers are generated for the exporter's sake | changeset | files |