diff --git a/.gitignore b/.gitignore index 76301f0c..ea2c377b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ _build _opam +*.tmp