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