From d9da46b256e94846b11b5b737c9dfd4636998ba7 Mon Sep 17 00:00:00 2001
From: Rudolf Hornig <rudi@omnetpp.org>
Date: Thu, 28 Mar 2024 19:46:39 +0100
Subject: [PATCH] doc: on live github deployment do not use the .html suffix in
 link

github can server 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": {