Merge branch 'dev' into group-rework

This commit is contained in:
Nick O'Leary
2023-03-02 15:26:01 +00:00
committed by GitHub
18 changed files with 298 additions and 76 deletions

View File

@@ -105,6 +105,15 @@
}
}
}
.red-ui-tab:not(.red-ui-workspace-changed) .red-ui-flow-tab-changed {
display: none;
}
.red-ui-tab.red-ui-workspace-changed .red-ui-flow-tab-changed {
display: inline-block;
position: absolute;
top: 1px;
right: 1px;
}
.red-ui-workspace-locked-icon {
display: none;