summaryrefslogtreecommitdiff
ModeNameSize
-rw-r--r--.gitignore11logplain
-rw-r--r--Bidir.agda4367logplain