diff -r 2a86c4c98622 -r 743984f4664e doc/symbols-texonly.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc/symbols-texonly.tex Fri Mar 28 08:36:08 2025 -0500 @@ -0,0 +1,15 @@ + +\renewrobustcmd{\downto}{{{\mathchoice% + {\rotatebox[origin=c]{-20}{$\to$}}% display + {\rotatebox[origin=c]{-20}{$\to$}}% text + {\rotatebox[origin=c]{-20}{\scalebox{0.75}{$\to$}}}% subscript + {\rotatebox[origin=c]{-20}{\scalebox{0.6}{$\to$}}}% subsubscript +}}} + +\renewrobustcmd{\upto}{{{\mathchoice% + {\rotatebox[origin=c]{20}{$\to$}}% display + {\rotatebox[origin=c]{20}{$\to$}}% text + {\rotatebox[origin=c]{20}{\scalebox{0.75}{$\to$}}}% subscript + {\rotatebox[origin=c]{20}{\scalebox{0.6}{$\to$}}}% subsubscript +}}} +