summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2021-12-27 17:21:32 +0000
committerGreg Brown <greg.brown@cl.cam.ac.uk>2021-12-27 17:44:55 +0000
commit87913c4014f01a23d608457e379b74aa1befd4ab (patch)
tree34d2405463757cf44089a795adb9a932e6707e50 /.gitignore
parent0b581ec922b40284291d6814578bd2e68049c8b7 (diff)
Introduce Everything.agda to aid in overall compilation.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions