From fa85e06f4739d86103b1b009a12efec87577f829 Mon Sep 17 00:00:00 2001
From: Li Xuanji <xuanji@duolingo.com>
Date: Sun, 3 Aug 2025 01:34:19 -0400
Subject: [PATCH] Disable wavy red underline for errors

---
 book/static_files/style.css | 7 ++++++-
 serve.py                    | 2 +-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/book/static_files/style.css b/book/static_files/style.css
index 00c5aa2..6c09f6d 100644
--- a/book/static_files/style.css
+++ b/book/static_files/style.css
@@ -58,4 +58,9 @@ div.declaration {
     padding-bottom: 1em;
     margin-top: 1em;
     margin-bottom: 1em;
-}
\ No newline at end of file
+}
+
+/* HACK: disable wavy red underline for errors, because they are quite common in docstrings */
+.hl.lean .has-info.error :not(.tactic-state):not(.tactic-state *) {
+    text-decoration: none !important;
+}
diff --git a/serve.py b/serve.py
index aa99358..b250832 100644
--- a/serve.py
+++ b/serve.py
@@ -23,7 +23,7 @@ if __name__ == '__main__':
     PORT = 8000
     handler = CustomHTTPRequestHandler
     with HTTPServer(("", PORT), handler) as httpd:
-        print(f"Serving at http://localhost:{PORT}/analysis")
+        print(f"Serving at http://localhost:{PORT}/analysis/")
         print(f"/analysis: {BOOK_SITE}")
         print(f"/analysis/docs: {DOCS_SITE}")
         httpd.serve_forever()
-- 
2.51.2