diff --git a/documentation/.gitignore b/documentation/.gitignore index 69fa449dd9..21bb72530a 100644 --- a/documentation/.gitignore +++ b/documentation/.gitignore @@ -1 +1,2 @@ _build/ +Pipfile.lock diff --git a/documentation/Pipfile b/documentation/Pipfile new file mode 100644 index 0000000000..7ee1d22905 --- /dev/null +++ b/documentation/Pipfile @@ -0,0 +1,14 @@ +[[source]] +name = "pypi" +url = "https://pypi.org/simple" +verify_ssl = true + +[dev-packages] + +[packages] +sphinx = "*" +sphinx-rtd-theme = "*" +pyyaml = "*" + +[requires] +python_version = "3" diff --git a/documentation/README b/documentation/README index 534ae66f86..28d5c4be8e 100644 --- a/documentation/README +++ b/documentation/README @@ -127,6 +127,13 @@ The resulting HTML index page will be _build/html/index.html, and you can browse your own copy of the locally generated documentation with your browser. +Alternatively, you can use Pipenv to automatically install all required +dependencies in a virtual environment: + + $ cd documentation + $ pipenv install + $ pipenv run make html + Sphinx theme and CSS customization ==================================