diff --git a/mps/.readthedocs.yaml b/mps/.readthedocs.yaml new file mode 100644 index 00000000000..7e1388f334b --- /dev/null +++ b/mps/.readthedocs.yaml @@ -0,0 +1,16 @@ +# .readthedocs.yaml -- Build configuration for MPS manual on Read The Docs +# +# See https://docs.readthedocs.io/en/stable/config-file/v2.html + +version: 2 + +formats: all + +build: + os: ubuntu-22.04 + tools: + python: 3 + +python: + install: + - requirements: manual/requirements.pip diff --git a/mps/manual/Makefile b/mps/manual/Makefile index 3781270fe34..9eded2625ef 100644 --- a/mps/manual/Makefile +++ b/mps/manual/Makefile @@ -2,6 +2,7 @@ # $Id$ # You can set these variables from the command line. +PYTHON = python3 SPHINXOPTS = SPHINXBUILD = tool/bin/sphinx-build PAPER = @@ -154,12 +155,11 @@ doctest: $(SPHINXBUILD) @echo "Testing of doctests in the sources finished, look at the " \ "results in $(BUILDDIR)/doctest/output.txt." -tools: tool/bin/sphinx-build +.PHONY: tools +tools: tool/bin/pip requirements.pip + tool/bin/pip install -r requirements.pip -tool/bin/sphinx-build: tool/bin/pip - tool/bin/pip install 'sphinx < 5' # Layout breaks in Sphinx >= 5. See . - @echo "You can now use \`make SPHINXBUILD=tool/bin/sphinx-build html' etc." - @echo "Or add tool/bin to your path." +tool/bin/sphinx-build: tools tool/bin/pip: - python3 -mvenv tool + $(PYTHON) -mvenv tool diff --git a/mps/manual/requirements.pip b/mps/manual/requirements.pip new file mode 100644 index 00000000000..f5e50bda3e1 --- /dev/null +++ b/mps/manual/requirements.pip @@ -0,0 +1,4 @@ +# manual/requirements.txt -- MPS manual build requirements for pip + +# Layout breaks in Sphinx >= 5. See . +sphinx >= 4, < 5