Allows to specify the port on which serve documentation (GH-31145)

[user@localhost]$ make serve      # default configuration, no change
python3 ../Tools/scripts/serve.py build/html
Serving build/html on port 8000, control-C to stop
^CShutting down.

[user@localhost]$ make serve SERVE_PORT=8080 # new option
python3 ../Tools/scripts/serve.py build/html 8080
Serving build/html on port 8080, control-C to stop
This commit is contained in:
Christophe Nanteuil 2022-02-06 11:22:06 +01:00 committed by GitHub
parent 96b344c2f1
commit f1e29cea85
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 1 deletions

View File

@ -12,6 +12,7 @@ PAPER =
SOURCES =
DISTVERSION = $(shell $(PYTHON) tools/extensions/patchlevel.py)
SPHINXERRORHANDLING = -W
SERVE_PORT =
# Internal variables.
PAPEROPT_a4 = -D latex_elements.papersize=a4paper
@ -217,7 +218,7 @@ check:
$(PYTHON) tools/rstlint.py ../Misc/NEWS.d/next/
serve:
$(PYTHON) ../Tools/scripts/serve.py build/html
$(PYTHON) ../Tools/scripts/serve.py build/html $(SERVE_PORT)
# Targets for daily automated doc build
# By default, Sphinx only rebuilds pages where the page content has changed.