We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 910852a commit deda371Copy full SHA for deda371
style/style.less
@@ -124,7 +124,11 @@
124
125
background: @header-background;
126
127
- line-height: @header-height;
+ // flexbox layout for proper alignment
128
+ display: flex;
129
+ justify-content: space-between;
130
+ align-items: center;
131
+
132
font-size: var(--agdaMode-buffer-font-size);
133
font-weight: bold;
134
@@ -143,8 +147,15 @@
143
147
.agda-mode-header-connection-status {
144
148
color: @foreground-subtle;
145
149
font-size: 50%;
146
- font-variant: small-caps;
- float: right
150
+ // font-variant: small-caps;
151
152
+ &.clickable {
153
+ cursor: pointer;
154
155
+ &:hover {
156
+ color: @foreground-highlight;
157
+ }
158
159
}
160
161
0 commit comments