Skip to content
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

Fix the man pages' formatting. #19058

Merged
merged 1 commit into from
May 23, 2024
Merged

Fix the man pages' formatting. #19058

merged 1 commit into from
May 23, 2024

Conversation

Humm42
Copy link

@Humm42 Humm42 commented May 21, 2024

I'm thinking about learning myself a little Coq, but there's a glaring rock in the way: The man pages are badly formatted. Can't possibly attempt to learn as long as they stay that way.

The main changes are these:

Empty lines emit vertical space; replace by stylistic no-ops or actual paragraph separators.

Wherever there should be a hyphen-minus in the output, use - in the input.

Tell troff where a sentence ends by following it by a newline.

Ellipses look nicer with a little space between the dots; do that.

The description in the NAME section shouldn't be capitalized and should be nicely readable.

Let the man page titles be what the man pages are about.

Don't use font-alternating macros where simple font-changing macros suffice.

There's more that I'd change if I were in control of the man pages, but that's less important. If you want more rationale for the things I did do, ask me. I'm happy to talk about troff.

I'm thinking about learning myself a little Coq, but there's a glaring
rock in the way: The man pages are badly formatted.  Can't possibly
attempt to learn as long as they stay that way.

The main changes are these:

Empty lines emit vertical space; replace by stylistic no-ops or actual
paragraph separators.

Wherever there should be a hyphen-minus in the output, use \- in the
input.

Tell troff where a sentence ends by following it by a newline.

Ellipses look nicer with a little space between the dots; do that.

The description in the NAME section shouldn't be capitalized and should
be nicely readable.

Let the man page titles be what the man pages are about.

Don't use font-alternating macros where simple font-changing macros
suffice.

There's more that I'd change if I were in control of the man pages, but
that's less important.  If you want more rationale for the things I did
do, ask me.  I'm happy to talk about troff.
@Humm42 Humm42 requested a review from a team as a code owner May 21, 2024 01:07
@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 May 21, 2024
@SkySkimmer SkySkimmer self-assigned this May 23, 2024
@SkySkimmer SkySkimmer added kind: documentation Additions or improvement to documentation. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels May 23, 2024
@SkySkimmer SkySkimmer added this to the 8.20+rc1 milestone May 23, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 566751f into coq:master May 23, 2024
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: documentation Additions or improvement to documentation.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants