diff --git a/.gitignore b/.gitignore index 322ae6a8a0c3c231973c8b421c61f7ee462e0ce4..a223f300c9785e70eecfa9068e4bad4ea15f109a 100644 --- a/.gitignore +++ b/.gitignore @@ -98,8 +98,7 @@ _darcs/ /docs/users_guide/users_guide.pdf /docs/users_guide/build-html /docs/users_guide/build-pdf -/docs/users_guide/.doctrees-html -/docs/users_guide/.doctrees-pdf +/docs/users_guide/.doctrees-* /driver/ghci/ghc-pkg-inplace /driver/ghci/ghci-inplace /driver/ghci/ghci.res diff --git a/docs/users_guide/ghc.mk b/docs/users_guide/ghc.mk index 1d48fa157a56615b49d06a24f3dbc83d01cabf48..deb60a342f3dd61e17c3f26395069d1fefa61960 100644 --- a/docs/users_guide/ghc.mk +++ b/docs/users_guide/ghc.mk @@ -27,7 +27,7 @@ MAN_PAGES := docs/users_guide/ghc.1 ifneq "$(BINDIST)" "YES" $(MAN_PAGES): $(docs/users_guide_MAN_RST_SOURCES) $(utils/mkUserGuidePart_GENERATED_RST_SOURCES) - $(SPHINXBUILD) -b man docs/users_guide docs/users_guide + $(SPHINXBUILD) -b man -d docs/users_guide/.doctrees-man docs/users_guide docs/users_guide endif man : $(MAN_PAGES)