Commit 1986eda4 authored by Richard Berger's avatar Richard Berger
Browse files

Remove no longer needed generated files in doc

If we use the Google Custom Search API, we do not need to keep the
generated searchindex.js file anymore. We also can safely remove
the _sources directory for good.

Since these get generated during each Sphinx build, additional
steps have been added to the Makefile to get rid of them. They
are also added to .gitignore to avoid commiting them by accident.
parent e71fafdd
Loading
Loading
Loading
Loading
+3 −1
Original line number Diff line number Diff line
@@ -43,6 +43,8 @@ html: $(OBJECTS)
		sphinx-build -j 8 -b html -c utils/sphinx-config -d $(BUILDDIR)/doctrees $(RSTDIR) html ;\
		deactivate ;\
	)
	-rm html/searchindex.js
	-rm -rf html/_sources
	@echo "Build finished. The HTML pages are in doc/html."

pdf: utils/txt2html/txt2html.exe
+2 −0
Original line number Diff line number Diff line
.buildinfo
objects.inv
searchindex.js
_sources

doc/html/searchindex.js

deleted100644 → 0
+0 −1

File deleted.

Preview size limit exceeded, changes collapsed.