From 8f12aab3b083ab646148e734efe85cec7527776b Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sun, 16 Jul 2023 18:54:11 +0200
Subject: [PATCH] scroll if hidden hints are toggled

---
 client/src/components/level.tsx | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 439aea9..be2165f 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -93,7 +93,7 @@ function PlayableLevel({worldId, levelId}) {
     // TODO: For some reason this is always called twice
     console.debug('scroll chat')
     chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0)
-  }, [proof])
+  }, [proof, showHiddenHints])
 
   React.useEffect(() => {
     if (!commandLineMode) {