From 4803bcccd40aff72956971f1479ecedcbc6cec32 Mon Sep 17 00:00:00 2001 From: dominik003 Date: Mon, 9 Oct 2023 13:28:33 +0200 Subject: [PATCH] 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. --- docs/user/mkdocs.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/docs/user/mkdocs.yml b/docs/user/mkdocs.yml index 11362b611..fa3c9652e 100644 --- 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 © 2022-2023 DB Netz AG