Fix bug that allowed following multiple people in one pane (#3108)

I've also simplified the representation of a workspace's leaders, so
that it encodes in the type that there can only be one leader per pane.

Release Notes:

- Fixed a bug where you could accidentally follow multiple collaborators
in one pane at the same time.
6b710dc146Max Brunsfeld committed on 10/9/2023, 8:50:51 PM· committed by GitHubparents0823a18ca735ad
3 files changedLine totals unavailable