summaryrefslogtreecommitdiff
path: root/.gitignore
blob: c6a4dc30d78eacbcc03f8154cf281e9637c942d3 (plain)
1
2
3
4
5
6


*.cmi
*.cmx
*.o