aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/.gitignore
blob: 3e4978fac48d6aaea3257560b32ce727fc0cf882 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
*.ml*.d
*.cm[ixt]*
Makefile.coq*
*~
*.[ao]
.coqdeps.d
*.vo
*.glob
*.aux
*/*/.merlin

# by convention g_foo.ml is generated
g_*.ml