From 6224cd40d44b8d434c10cae1e49389d7824057ba Mon Sep 17 00:00:00 2001
From: Felix Roos <flix91@gmail.com>
Date: Sun, 21 Jan 2024 01:21:13 +0100
Subject: [PATCH] mini repl max height option

---
 website/src/docs/MiniRepl.jsx | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/website/src/docs/MiniRepl.jsx b/website/src/docs/MiniRepl.jsx
index 10eff483..3afb609e 100644
--- a/website/src/docs/MiniRepl.jsx
+++ b/website/src/docs/MiniRepl.jsx
@@ -27,6 +27,7 @@ export function MiniRepl({
   punchcardLabels = true,
   claviature,
   claviatureLabels,
+  maxHeight,
 }) {
   const code = tunes ? tunes[0] : tune;
   const id = useMemo(() => s4(), []);
@@ -154,7 +155,7 @@ export function MiniRepl({
           )}
         </div>
       )}
-      <div className="overflow-auto relative p-1">
+      <div className="overflow-auto relative p-1" style={maxHeight ? { maxHeight: `${maxHeight}px` } : {}}>
         <div
           ref={(el) => {
             if (!editorRef.current) {