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

Docs are missing for e.g. contrib.Text.* #4047

Closed
hejfelix opened this issue Sep 3, 2017 · 5 comments
Closed

Docs are missing for e.g. contrib.Text.* #4047

hejfelix opened this issue Sep 3, 2017 · 5 comments

Comments

@hejfelix
Copy link

hejfelix commented Sep 3, 2017

While searching the contrib docs for the Text.PrettyPrint module, I realized that it's missing.

Does the module not follow the docs syntax or is it simply missing from the build?

@jfdm
Copy link
Contributor

jfdm commented Sep 3, 2017

Missing from the build, or the docs are for a version of contrib prior to the inclusion of the Pretty.Print module. Those docs are published by hand. With installed version's of Idris the docs are stored locally in idris --libdocdir (I think that is the correct flag).

@melted
Copy link
Contributor

melted commented Sep 3, 2017

It could be this bug #2161

I have a diagnosis, but my solution needs a bit of work.

@jfdm
Copy link
Contributor

jfdm commented Sep 3, 2017

@melted those docs are for Idris contrib v1.0. PrettyPrint wasn't included until v1.1 or newer.

@melted
Copy link
Contributor

melted commented Sep 4, 2017 via email

@jfdm
Copy link
Contributor

jfdm commented Nov 9, 2017

I am going to close this issue, as the pointed to idris docs were for a version of idris prior to inclusion of the pretty printer.

@jfdm jfdm closed this as completed Nov 9, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants