diff --git a/.gitignore b/.gitignore index 2b1d09c9de1..1a3bfef2a02 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ # local and generated files not to be committed +doc/src/showcases +doc/src/tutorials src/Makefile -src/Makefile.vc *_m.h *_m.cc *_sm.h diff --git a/doc/src/Makefile b/doc/src/Makefile index 32df6949afc..5e58e9834b6 100644 --- a/doc/src/Makefile +++ b/doc/src/Makefile @@ -18,12 +18,15 @@ help: include tools/sphinx_deployment.mk server: Makefile copy-media + ln -sf ../../showcases showcases; ln -sf ../../tutorials @sphinx-autobuild --host 0.0.0.0 --port 8000 "$(SOURCEDIR)" "$(BUILDDIR)/html" $(SPHINXOPTS) $(O) -r .git pdf: Makefile copy-media + ln -sf ../../showcases showcases; ln -sf ../../tutorials @$(SPHINXBUILD) -M latexpdf "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) html: Makefile copy-media + ln -sf ../../showcases showcases; ln -sf ../../tutorials @$(SPHINXBUILD) -M html "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) copy-media: ../../media