summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2023-07-07 17:40:03 +0100
committerGreg Brown <greg.brown01@ed.ac.uk>2023-07-07 17:40:03 +0100
commitd42c29c3ded0e48021b24295c925b88232df6b75 (patch)
treeca4a7551e46c4e813cff464ea6acbd74b90d9c99 /.gitignore
parent6b637a6d2954e77985e24bbd17f3697eb6f8238a (diff)
Add occurs check for terms.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions