diff options
Diffstat (limited to 'Documentation/infrastructure/index.md')
| -rw-r--r-- | Documentation/infrastructure/index.md | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/Documentation/infrastructure/index.md b/Documentation/infrastructure/index.md index 6748637762..75ad61b506 100644 --- a/Documentation/infrastructure/index.md +++ b/Documentation/infrastructure/index.md @@ -4,9 +4,17 @@ This section contains documentation about our infrastructure ## Services -* [Project services](services.md) -* [Administrator's handbook](admin.md) +```{toctree} +:maxdepth: 1 + +Project services <services.md> +Administrator's handbook <admin.md> +``` ## Jenkins builders and builds -* [Setting up Jenkins build machines](builders.md) -* [Coverity Scan integration](coverity.md) +```{toctree} +:maxdepth: 1 + +Setting up Jenkins build machines <builders.md> +Coverity Scan integration <coverity.md> +``` |