summaryrefslogtreecommitdiff
path: root/tools
ModeNameSize
-rw-r--r--Scanner.lean1320logplain
d---------Scanner80logplain