diff -r ab9d03750630 -r bab81cf591a5 docs/src/header.html --- a/docs/src/header.html Tue Jun 20 19:00:52 2023 +0200 +++ b/docs/src/header.html Tue Jun 20 19:04:07 2023 +0200 @@ -18,9 +18,21 @@