diff --git a/.gitignore b/.gitignore index 8eb29ec2a0b14a59658635f4b9dd8954f871775f..c94f158420ebde64e8e896a0f88c3e6752877fe1 100644 --- a/.gitignore +++ b/.gitignore @@ -18,5 +18,7 @@ *.agdai *.agda~ +paper-new/paper.pdf + diff --git a/paper-new/paper.pdf b/paper-new/paper.pdf deleted file mode 100644 index c86537d615c0a4764a703e1d8b1c9c23e7bf844d..0000000000000000000000000000000000000000 Binary files a/paper-new/paper.pdf and /dev/null differ