
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
+}}}
+




