Explorar o código

fix double-remote-caret (#10315)

Kevin Jahns %!s(int64=4) %!d(string=hai) anos
pai
achega
f0a86822f7
Modificáronse 1 ficheiros con 2 adicións e 3 borrados
  1. 2 3
      packages/codemirror/style/base.css

+ 2 - 3
packages/codemirror/style/base.css

@@ -230,8 +230,7 @@
 /* Styles for shared cursors (remote cursor locations and selected ranges) */
 .jp-CodeMirrorEditor .remote-caret {
   position: relative;
-  border-left: 1px solid black;
-  border-right: 1px solid black;
+  border-left: 2px solid black;
   margin-left: -1px;
   margin-right: -1px;
   box-sizing: border-box;
@@ -240,7 +239,7 @@
 .jp-CodeMirrorEditor .remote-caret > div {
   position: absolute;
   top: -1.05em;
-  left: -1px;
+  left: -2px;
   font-size: 0.8em;
   background-color: rgb(250, 129, 0);
   font-family: serif;