gitignore: Ignore sphinx doctrees directories
authorBen Gamari <ben@smart-cactus.org>
Fri, 23 Oct 2015 10:06:59 +0000 (12:06 +0200)
committerBen Gamari <ben@smart-cactus.org>
Fri, 23 Oct 2015 15:44:00 +0000 (17:44 +0200)
.gitignore

index 20fb883..33664d7 100644 (file)
@@ -98,7 +98,8 @@ _darcs/
 /docs/users_guide/users_guide.pdf
 /docs/users_guide/build-html
 /docs/users_guide/build-pdf
-/docs/users_guide/.doctrees
+/docs/users_guide/.doctrees-html
+/docs/users_guide/.doctrees-pdf
 /driver/ghci/ghc-pkg-inplace
 /driver/ghci/ghci-inplace
 /driver/ghci/ghci.res