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.

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

Generate HTML files #25

Open
1 task
yurrriq opened this issue Jul 20, 2017 · 3 comments
Open
1 task

Generate HTML files #25

yurrriq opened this issue Jul 20, 2017 · 3 comments
Labels
enhancement help wanted
Milestone
First ten chapters

Comments

@yurrriq
Copy link
Collaborator

yurrriq commented Jul 20, 2017 •
edited
Loading

  • Do we want these?
  • Should we host them on the site too?
  • This will require updating pandoc-minted.hs to support HTML
  • link them on the site
@yurrriq yurrriq mentioned this issue Jul 20, 2017
Open
@david-christiansen
Copy link
Member

Why not highlight Idris code using the Idris compiler's notion of highlighting, rather than relying on syntax only?
https://github.com/david-christiansen/idris-code-highlighter is a start for this, though it could be made more friendly!

@yurrriq
Copy link
Collaborator Author

yurrriq commented Jul 20, 2017

That's a great idea!

@yurrriq yurrriq mentioned this issue Jul 25, 2017
Open
@yurrriq yurrriq mentioned this issue Aug 3, 2017
Closed
@yurrriq
Copy link
Collaborator Author

yurrriq commented Aug 3, 2017

Related: #30

@yurrriq yurrriq added this to the First ten chapters milestone Aug 3, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement help wanted
Projects
None yet
Milestone
First ten chapters
Development

No branches or pull requests
2 participants
@david-christiansen @yurrriq