+ disable cursor blink

+ make cursor thicker
2023-06-11 20:21:11 +02:00 · 2023-06-11 20:21:11 +02:00 · 370d82e66c
commit 370d82e66c
parent 876e851517
2 changed files with 16 additions and 0 deletions
--- a/website/src/docs/MiniRepl.css
+++ b/website/src/docs/MiniRepl.css
@ -16,3 +16,11 @@
 .cm-gutters {
  display: none !important;
 }
+
+.cm-cursorLayer {
+  animation-name: inherit !important;
+}
+
+.cm-cursor {
+  border-left: 2px solid currentcolor !important;
+}