chore: Change mkdocs local dev port

This sets the port when running mkdocs to 8081, so as not to interfere with a running backend on 8080.
DSD-DBS · Oct 9, 2023 · 6433272 · 6433272
1 parent fa73955
commit 6433272
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/docs/user/mkdocs.yml b/docs/user/mkdocs.yml
@@ -53,6 +53,7 @@ nav:
           - pure::variants: settings/tools/pure_variants.md
       - Model sources:
           - Git: settings/model-sources/git.md
+          - T4C: settings/model-sources/t4c.md
       - Alerts:
           - Create an alert: additional/alerts/create.md
           - Delete an alert: additional/alerts/delete.md
@@ -92,4 +93,6 @@ markdown_extensions:
 extra:
   generator: false
 
+dev_addr: 127.0.0.1:8081
+
 copyright: Copyright &copy; 2022-2023 DB Netz AG