diff --git a/.gitignore b/.gitignore index 038ac32a55..bf4bd454b1 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ favicon.* home.html addon *~ +robots.txt #ignore documentation, it should be newly built doc/api