diff options
| -rw-r--r-- | .gitignore | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 81a332a344..88e49f2c11 100644 --- a/.gitignore +++ b/.gitignore @@ -4,9 +4,10 @@ *.vo *.cm* *.annot +*.spit +*.spot *.o *.a -*.annot *.log *.aux *.dvi @@ -98,3 +99,4 @@ dev/doc/naming-conventions.pdf _build plugins/*/*_mod.ml myocamlbuild_config.ml +.DS_Store |