Merge pull request #1356 from zed-industries/differentiate-same-tab-titles

Differentiate among tabs with the same name
This commit is contained in:
Antonio Scandurra
2022-07-15 08:30:22 +02:00
committed by GitHub
12 changed files with 248 additions and 28 deletions
+4
View File
@@ -27,6 +27,10 @@ export default function workspace(theme: Theme) {
left: 8,
right: 8,
},
description: {
margin: { left: 6, top: 1 },
...text(theme, "sans", "muted", { size: "2xs" })
}
};
const activeTab = {