From 53d755ff54927592849fe85886085c5806d59f60 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 14 Jan 2025 11:19:55 +0100
Subject: [PATCH] fmt

---
 docs/javascripts/hax_playground.js  | 13 +++++++------
 docs/stylesheets/hax_playground.css | 10 +---------
 2 files changed, 8 insertions(+), 15 deletions(-)

diff --git a/docs/javascripts/hax_playground.js b/docs/javascripts/hax_playground.js
index 5ef4b3dd0..6a8b56727 100644
--- a/docs/javascripts/hax_playground.js
+++ b/docs/javascripts/hax_playground.js
@@ -135,12 +135,13 @@ function setup() {
         button_tc.classList.add('md-hax-playground');
         button_tc.style.right = "4.5em";
         button_tc.onclick = () => {
-            call_playground(result_block, 'fstar+tc', getCode());
-        };
-        e.prepend(button_tc);
+            button_tc.onclick = () => {
+                call_playground(result_block, 'fstar+tc', getCode());
+            };
+            e.prepend(button_tc);
 
-        code.style.padding = "0 0.9em";
+            code.style.padding = "0 0.9em";
+        }
     }
-}
 
-setup();
+    setup();
diff --git a/docs/stylesheets/hax_playground.css b/docs/stylesheets/hax_playground.css
index c48e8cf9e..dbf4eeace 100644
--- a/docs/stylesheets/hax_playground.css
+++ b/docs/stylesheets/hax_playground.css
@@ -1,11 +1,3 @@
 .md-hax-playground::after {
     display: none;
-}
-
-font-family: "Monaco",
-"Menlo",
-"Ubuntu Mono",
-"Consolas",
-"Source Code Pro",
-"source-code-pro",
-monospace;
\ No newline at end of file
+}
\ No newline at end of file