From fbec9c13aa16df603deaebf575acb3ebb6e3f5b9 Mon Sep 17 00:00:00 2001 From: baldurk Date: Mon, 6 Aug 2018 17:00:48 +0100 Subject: [PATCH] If sphinx_rtd_theme_chm_friendly directory is missing, use normal theme --- docs/conf.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index f2962b06d..7f1a3217e 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -320,8 +320,11 @@ texinfo_documents = [ #texinfo_no_detailmenu = False # custom theme based on sphinx_rtd_theme -html_theme = "sphinx_rtd_theme_chm_friendly" -html_theme_path = ["."] +if os.path.isdir('sphinx_rtd_theme_chm_friendly'): + html_theme = "sphinx_rtd_theme_chm_friendly" + html_theme_path = ["."] +else: + html_theme = "sphinx_rtd_theme" html_context = { 'show_source': False,