summaryrefslogtreecommitdiff
path: root/tools
ModeNameSize
-rw-r--r--Scanner.lean2579logplain
d---------Scanner194logplain