aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/using/tools
ModeNameSize
-rw-r--r--coqdoc.rst15413logplain
-rw-r--r--index.rst717logplain