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

@@ -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": {