aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
ModeNameSize
-rw-r--r--Makefile1442logplain
-rw-r--r--ProofGeneral.texi22659logplain
-rw-r--r--dir619logplain
-rw-r--r--localdir69logplain