From 0e82fb8c47b527ee8692b979c86959d238338e90 Mon Sep 17 00:00:00 2001 From: Fabian Homborg Date: Mon, 25 Feb 2019 21:05:02 +0100 Subject: [PATCH] Install sphinx files Sphinx put the files into sphinx-root, which wasn't being installed. Instead, use user_doc again, which we already used before. Belongs to #5696. --- cmake/Docs.cmake | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cmake/Docs.cmake b/cmake/Docs.cmake index 4d2774e8a..0d30abba0 100644 --- a/cmake/Docs.cmake +++ b/cmake/Docs.cmake @@ -7,7 +7,7 @@ FIND_PROGRAM(SPHINX_EXECUTABLE NAMES sphinx-build INCLUDE(FeatureSummary) SET(SPHINX_SRC_DIR "${CMAKE_CURRENT_SOURCE_DIR}/sphinx_doc_src") -SET(SPHINX_ROOT_DIR "${CMAKE_CURRENT_BINARY_DIR}/sphinx-root") +SET(SPHINX_ROOT_DIR "${CMAKE_CURRENT_BINARY_DIR}/user_doc") SET(SPHINX_BUILD_DIR "${SPHINX_ROOT_DIR}/build") SET(SPHINX_CACHE_DIR "${SPHINX_ROOT_DIR}/doctrees") SET(SPHINX_HTML_DIR "${SPHINX_ROOT_DIR}/html")