Skip to content

Fix #20679: avoid spurious newline in rocqdoc blocks. #20710

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.

Sign up for GitHub

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

Jump to bottom
Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix #20679: avoid spurious newline in rocqdoc blocks. #20710

wants to merge 1 commit into from

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Jun 4, 2025

Adjust the CSS selectors of rocqdoc to be closer to the ones of rocqtop.

Fix #20679

@Zimmi48
Fix rocq-prover#20679: avoid spurious newline in rocqdoc blocks.
1a7a153 
Adjust the CSS selectors of rocqdoc to be closer to the ones of rocqtop.
@Zimmi48 Zimmi48 added this to the 9.0.1 milestone Jun 4, 2025
@Zimmi48 Zimmi48 requested a review from a team as a code owner June 4, 2025 18:13
@Zimmi48 Zimmi48 added kind: documentation Additions or improvement to documentation. kind: infrastructure CI, build tools, development tools. labels Jun 4, 2025
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 4, 2025
@Villetaneuse
Copy link
Contributor

Rendered: https://coq.gitlabpages.inria.fr/-/coq/-/jobs/5831318/artifacts/_build/default/doc/refman-html/index.html

@Villetaneuse Villetaneuse removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 5, 2025
@Villetaneuse
Copy link
Contributor

There are still some spurious lines here and there...
See for instance this : https://coq.gitlabpages.inria.fr/-/coq/-/jobs/5831318/artifacts/_build/default/doc/refman-html/language/core/records.html
after "Compare to Record in the previous example:"
Don't know if we should address it now or keep it for later.
In the html, the newline is made by an empty span element

<span></span>

@Villetaneuse
Copy link
Contributor

However it's clearly better now, so maybe just merge and get done with it?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: documentation Additions or improvement to documentation. kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
9.0.1
Development

Successfully merging this pull request may close these issues.

rocdoc directive inserts an extra blank line in doc, doesn't look right
2 participants
@Zimmi48 @Villetaneuse