New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Added a header to mathlib index #140
Conversation
templates/index.j2
Outdated
<ul> | ||
<li>mathlib <a href="{{ mathlib_github_root }}/tree/{{ mathlib_commit }}">{{ mathlib_commit }}</a></li> | ||
<li>Lean <a href="https://github.com/leanprover-community/lean/blob/{{ lean_commit }}/library">{{ lean_commit }}</a></li> | ||
</ul> | ||
|
||
<p>Note: mathlib is still only partially documented, and this HTML display is still |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you're already cleaning up the front page, then I would also remove this part.
<p>Note: mathlib is still only partially documented, and this HTML display is still | |
<p> |
templates/index.j2
Outdated
|
||
{% block content %} | ||
<h1>Welcome to mathlib's documentation page</h1> | ||
|
||
<p>Navigate through mathlib files using the menu on the left.</p> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think Partick already mentioned this on zulip, but it would be good to clarify at this point that this is the automatically-generated documentation from the docstrings in mathlib, and include a link to the main site.
#deploy |
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
#deploy |
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! |
Also mentioned commit hashes in list items for easier readability
Closes #138