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