diff options
Diffstat (limited to 'doc/plugin_tutorial/.gitignore')
| -rw-r--r-- | doc/plugin_tutorial/.gitignore | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/doc/plugin_tutorial/.gitignore b/doc/plugin_tutorial/.gitignore new file mode 100644 index 0000000000..3e4978fac4 --- /dev/null +++ b/doc/plugin_tutorial/.gitignore @@ -0,0 +1,13 @@ +*.ml*.d +*.cm[ixt]* +Makefile.coq* +*~ +*.[ao] +.coqdeps.d +*.vo +*.glob +*.aux +*/*/.merlin + +# by convention g_foo.ml is generated +g_*.ml |