Fix the height and move the navigation arrows #2

Manually merged

pilou merged 2 commits from fix_header_height_and_move_nav_arrows into main

2022-07-16 03:42:12 +02:00

Author	SHA1	Message	Date
Pierre-Louis Bonicoli	1079256dc1	Don't hide 'settings' tab with the nav arrows Ref #5851	2022-07-16 03:34:18 +02:00
Pierre-Louis Bonicoli	eb8dd4c297	div#header: fully display title of subprojects Ref #5851	2022-07-16 03:30:47 +02:00