Show module docstring for namespace indexes #3351
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Matthew-Mosior
changed the title
2 tasks
TODO: add a common.css for these shared parts?
|
I've got a few fixes, do you mind authorising pushes from Idris2 maintainers on this PR? |
No problem, just allowed that! |
gallais
force-pushed
the
issue-3014-show-module-docstring-for-namespace-indexes
branch
2 times, most recently
from
0c2f765
to
d25e6d9
Compare
gallais
force-pushed
the
issue-3014-show-module-docstring-for-namespace-indexes
branch
from
d25e6d9
to
61535f7
Compare
|
I've fixed as many linting issues as I could. If someone wants to figure out that
then PRs are welcome. |
gallais
added
documentation
|
@gallais I didn't realize there was linting run on the repo, my apologies |
|
No worries, most of the linting issues were introduced by me :D |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR addresses 3014 and adds functionality for adding docstrings for each applicable module when created via
--mkdoc.Closes #3014.