merge

2022-03-16 11:39:34 -04:00
parent b4de2787c7 8b32d0c8ba
commit f678f0824b
16 changed files with 613 additions and 201 deletions
@@ -180,6 +180,12 @@
 }

 .xterm-find-result-decoration {
-   background-color: blue;
+   background-color: yellow;
   opacity: 60%;
-}
+}
+.xterm-decoration-overview-ruler {
+    z-index: 7;
+    position: absolute;
+    top: 0;
+    right: 0;
+}