Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

IdrisDoc and Package Installation #1249

Closed
jfdm opened this issue May 21, 2014 · 1 comment
Closed

IdrisDoc and Package Installation #1249

jfdm opened this issue May 21, 2014 · 1 comment
Labels
C-Low Hanging Fruit Z-Feature Request

Comments

@jfdm
Copy link
Contributor

jfdm commented May 21, 2014

We now have a HTML documentation generation system. When installing Idris packages the package's HTML documentation should be generated and installed into a single well-known place.

Problems:

  1. Where is this 'well-known' place?
  2. Auto-generation of a suitable landing page for this documentation.
  3. When installing packages should we have the option to switch of documentation generation?
@jfdm
Copy link
Contributor Author

jfdm commented Dec 6, 2016

Erm I addressed this in PR #3462 , and forgot to close this issue.

@jfdm jfdm closed this as completed Dec 6, 2016
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
C-Low Hanging Fruit Z-Feature Request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jfdm @ahmadsalim