summaryrefslogtreecommitdiff
path: root/tools
ModeNameSize
-rw-r--r--Scanner.lean1439logplain
d---------Scanner122logplain