Skip to content

Commit

Permalink
doc: on live github deployment do not use the .html suffix in link
Browse files Browse the repository at this point in the history
github can server the same page with and without the .html suffix
so we opt to use nicer URLs without the .html suffix
  • Loading branch information
rhornig committed Mar 28, 2024
1 parent 2f59a93 commit d9da46b
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions doc/src/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -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": {
Expand Down

0 comments on commit d9da46b

Please sign in to comment.