diff --git a/Idris.gitignore b/Idris.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..c28bc7cc675f54a316a8944d22674529b9d21210 --- /dev/null +++ b/Idris.gitignore @@ -0,0 +1,2 @@ +*.ibc +*.o