diff --git a/.gitignore b/.gitignore index 59dc76d..2377a8d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,13 +1,2 @@ -*.cmi -*.cmo -*.cma -*.cmx -*.cmxa -*.top -*.o -*.a -._bcdi/ -._ncdi/ -._d/ -cpdf -*.annot +.DS_Store +.texpadtmp