Allow customizing the pane's following border width in the theme

2022-03-22 13:32:25 -07:00
parent 4ed8f6fbb4
commit c105802b2d
3 changed files with 4 additions and 2 deletions
@@ -111,7 +111,7 @@ impl Member {
                        .editor
                        .replica_selection_style(leader.replica_id)
                        .cursor;
-                    border = Border::all(1.0, leader_color);
+                    border = Border::all(theme.workspace.leader_border_width, leader_color);
                    border
                        .color
                        .fade_out(1. - theme.workspace.leader_border_opacity);