From 370d82e66c6691e1e5b3044de2df8772b6be1270 Mon Sep 17 00:00:00 2001
From: Felix Roos <flix91@gmail.com>
Date: Sun, 11 Jun 2023 20:21:11 +0200
Subject: [PATCH] + disable cursor blink + make cursor thicker

---
 website/src/docs/MiniRepl.css | 8 ++++++++
 website/src/repl/Repl.css     | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/website/src/docs/MiniRepl.css b/website/src/docs/MiniRepl.css
index 8ec75d4d..84927a88 100644
--- 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;
+}
diff --git a/website/src/repl/Repl.css b/website/src/repl/Repl.css
index 6815966b..f7227d7d 100644
--- a/website/src/repl/Repl.css
+++ b/website/src/repl/Repl.css
@@ -45,3 +45,11 @@
 #code .cm-theme-light {
   width: 100%;
 }
+
+#code .cm-cursorLayer {
+  animation-name: inherit !important;
+}
+
+#code .cm-cursor {
+  border-left: 2px solid currentcolor !important;
+}