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