Fix wrong id being given to doc comments #1118
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
panglesd
force-pushed
the
fix-wrong-id-doc-search
branch
from
1e76109
to
58c3497
Compare
panglesd
added a commit
to panglesd/odoc
that referenced
this pull request
May 3, 2024
Signed-off-by: Paul-Elliot <peada@free.fr>
|
Always nice to see PRs that remove more lines than they add :-) |
|
I can't see clearly from the test what was broken before and now fixed? Is it worth having an explicit test? The sea of json in the existing test case is a bit meaningless right now. |
panglesd
added a commit
to panglesd/odoc
that referenced
this pull request
May 6, 2024
Signed-off-by: Paul-Elliot <peada@free.fr>
panglesd
force-pushed
the
fix-wrong-id-doc-search
branch
from
f9cbeb8
to
0d1a08e
Compare
panglesd
added a commit
to panglesd/odoc
that referenced
this pull request
May 6, 2024
Signed-off-by: Paul-Elliot <peada@free.fr>
panglesd
force-pushed
the
fix-wrong-id-doc-search
branch
from
0d1a08e
to
070110f
Compare
|
I added a more readable test focusing on the issue. |
Exhibit a bug! Signed-off-by: Paul-Elliot <peada@free.fr>
Standalone documentation comments currently do not have an id. This id was carried as the accumulator of the field, which yielded wrong results! Signed-off-by: Paul-Elliot <peada@free.fr>
Signed-off-by: Paul-Elliot <peada@free.fr>
Signed-off-by: Paul-Elliot <peada@free.fr>
panglesd
force-pushed
the
fix-wrong-id-doc-search
branch
from
070110f
to
073ae60
Compare
|
Ping @jonludlam @Julow |
|
Thanks! |
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.
Standalone documentation comments currently do not have an id. In search results, the goal was to give them the id of the signature they are in.
However, there was a confusion in the computation of this signature, resulting in a wrong ID. This PR fixes that.
The commit was originally in #1084 but since this PR does not seem to make a lot of progress, I think it is better to extract it in a standalone PR.