directory / @ 1:fa30a385957d default tip

name size permissions
file .hgignore 188 -rw-r--r--
file day.agda 2949 -rw-r--r--