diff options
| -rw-r--r-- | doc/developer/Makefile | 6 | ||||
| -rw-r--r-- | doc/user/Makefile | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/doc/developer/Makefile b/doc/developer/Makefile index 640a1ace38..f5e7cb60ec 100644 --- a/doc/developer/Makefile +++ b/doc/developer/Makefile @@ -2,9 +2,9 @@ # # You can set these variables from the command line. -SPHINXOPTS = -SPHINXBUILD = sphinx-build -PAPER = +SPHINXOPTS ?= +SPHINXBUILD ?= sphinx-build +PAPER ?= BUILDDIR = _build # User-friendly check for sphinx-build diff --git a/doc/user/Makefile b/doc/user/Makefile index 640a1ace38..f5e7cb60ec 100644 --- a/doc/user/Makefile +++ b/doc/user/Makefile @@ -2,9 +2,9 @@ # # You can set these variables from the command line. -SPHINXOPTS = -SPHINXBUILD = sphinx-build -PAPER = +SPHINXOPTS ?= +SPHINXBUILD ?= sphinx-build +PAPER ?= BUILDDIR = _build # User-friendly check for sphinx-build |