Merge branch 'dev' into groups

This commit is contained in:
Nick O'Leary
2020-03-30 23:42:52 +01:00
151 changed files with 5315 additions and 1453 deletions

View File

@@ -9,19 +9,15 @@
color: transparent !important;
}
}
.ace_gutter {
background: $text-editor-gutter-background;
border-top-left-radius: 4px;
border-bottom-left-radius: 4px;
}
.ace_scroller {
background: $text-editor-background;
border-top-right-radius: 4px;
border-bottom-right-radius: 4px;
}
.ace_scroller {
background: $text-editor-background;
color: $text-editor-color;
}
.ace_marker-layer .ace_active-line {
@@ -37,9 +33,6 @@
.ace_gutter-active-line {
background: $text-editor-gutter-active-line-background;
}
.ace_gutter {
background: $text-editor-gutter-background;
}
.ace_tooltip {
font-family: $primary-font;
line-height: 1.4em;

View File

@@ -32,6 +32,9 @@
right: 5px;
top: 9px;
}
form.red-ui-searchBox-form {
margin: 0;
}
input.red-ui-searchBox-input {
border-radius: 0;
border: none;

View File

@@ -112,7 +112,7 @@
position: absolute;
bottom: 0;
right:0;
zIndex: 101;
z-index: 101;
border-left: 1px solid $primary-border-color;
border-top: 1px solid $primary-border-color;
background: $view-navigator-background;
@@ -122,7 +122,7 @@
stroke-dasharray: 5,5;
pointer-events: none;
stroke: $secondary-border-color;
strokeWidth: 1;
stroke-width: 1;
fill: $view-background;
}