Merge pull request #264 from ldct/ldct-wavy

Disable wavy red underline for errors

book/static_files/style.css

···
     padding-bottom: 1em;
     margin-top: 1em;
     margin-bottom: 1em;
-}
+}
+
+/* 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;
+}

serve.py

···
     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()