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

Many missing manpages #15181

Open
SnarkBoojum opened this issue Nov 12, 2021 · 3 comments
Open

Many missing manpages #15181

SnarkBoojum opened this issue Nov 12, 2021 · 3 comments
Labels
kind: documentation Additions or improvement to documentation.

Comments

@SnarkBoojum
Copy link
Contributor

Here is a list of binary executables shipped with coq 8.14.0 without a manpage:

coqidetop
coqpp
coqproofworker
coqqueryworker
coqtacticworker
coqworkmgr
csdpcert
ocamllibdep
votour
@ppedrot
Copy link
Member

ppedrot commented Nov 12, 2021

Almost all of these binaries are for internal use and should not be called directly by the user. The only binary that would make sense to call in a shell is votour. Does it matter not to document internal binaries?

@SnarkBoojum
Copy link
Contributor Author

As long as they get installed in user-facing directories, they're not internal, so they should have a manpage.

I was told on zulpi that the make-* timing scripts would move to libexec in the next version -- all internal execs can probably go the same route, if they haven't already (I might be late to the party).

@ejgallego
Copy link
Member

This is almost a duplicate of #10613 , however there are indeed some binaries that are public and missing the man page.

@Alizter Alizter added the kind: documentation Additions or improvement to documentation. label Nov 17, 2021
@Alizter Alizter added this to Infrastructure in User documentation May 17, 2022
@Alizter Alizter moved this from Infrastructure to Writing in User documentation May 17, 2022
@Alizter Alizter moved this from Writing to Command line in User documentation May 25, 2022
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
Status: No status
User documentation
  
Command line
Development

No branches or pull requests

4 participants