Docs restructure (#2953)

Needs to be merged into `gh-pages` later on.
2023-05-30 10:02:53 +02:00 · 2023-05-30 10:02:53 +02:00 · f956a8c1d9
commit f956a8c1d9
parent 11b557097c
46 changed files with 447 additions and 855 deletions
--- a/docs/development/PROFILING.md
+++ b/docs/development/PROFILING.md
@ -1,6 +1,7 @@
 ---
 title: Profiling
 parent: Development
+nav_order: 4
 permalink: /development/profiling
 ---