v20240522-180622

[HUD] Add PR title to the page title (#5237)

Tried using `useEffect(()=> { document.title = "..."; }, []};` trick initially, but this does not seem to work reliable, so end up adding `DynamicTitle` component that defines a context(thank you ChatGPT for the hint on how to read React docs), and define `useSetTitle(title:string)` hook to update page title from the components

Also make title of top level HUD pages smaller