From 4d4f6a776a2bdf3763ae790d24e0db342fd3b877 Mon Sep 17 00:00:00 2001 From: Rudolf Hornig Date: Thu, 28 Mar 2024 19:46:39 +0100 Subject: [PATCH] doc: on live github deployment do not use the .html suffix in URLs github can serve the same page with and without the .html suffix so we opt to use nicer URLs without the .html suffix --- doc/src/conf.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/doc/src/conf.py b/doc/src/conf.py index abeb2b170..4b718d52c 100644 --- a/doc/src/conf.py +++ b/doc/src/conf.py @@ -165,6 +165,11 @@ def autodoc_skip_member_callback(app, what, name, obj, skip, options): html_logo = '_static/hero-banner.png' html_title = 'Simu5G: Simulator for 5G New Radio Networks' +# When building on github, we can use links without the .html suffix as github correctly displays those pages without the .html suffix +# During development, we need to use the .html suffix as local development does not work without it +if os.getenv("GITHUB_ACTIONS") == "true": + html_link_suffix = '' + # material theme options (see theme.conf for more information) html_theme_options = { "icon": {