Parameterize avatar_margin and assign it a default of 8

2022-05-03 18:04:53 +02:00 · 2022-05-03 18:04:53 +02:00 · 3ee4d90c19
commit 3ee4d90c19
parent c268099554
11 changed files with 11 additions and 1 deletions
--- a/crates/workspace/src/workspace.rs
+++ b/crates/workspace/src/workspace.rs
@ -1629,7 +1629,7 @@ impl Workspace {
            .constrained()
            .with_width(theme.workspace.titlebar.avatar_width)
            .contained()
-            .with_margin_left(2.)
+            .with_margin_left(theme.workspace.titlebar.avatar_margin)
            .boxed();

        if let Some(peer_id) = peer_id {