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

diff --git a/Doc/Makefile b/Doc/Makefile
index 19ddafc5f2f9fc7c6709dd8a7f16730abb04a32a..e60aa3427fea2474849398d82278c5c63bc7da45 100644 (file)
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -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.