-
Notifications
You must be signed in to change notification settings - Fork 20
Generate tutorial HTML automatically #780
Comments
I'm not so familiar with the doc workflow but can we have the generated files in a dedicated branch e.g. |
For this I think it is fine to manually generate the HTML and |
Current build instructions:
|
Thank you. I don't think we need the CI to automatically build the HTML (I am loathed to do anything to slow down the CI further). However, it would be good if the top level |
I believe it wouldn't slow down the CI -- if I understand correctly, the CI builds the core library and then builds the various subdirectories in parallel. This would be another pass that happens on top of the core library -- unless it's the very slowest of those targets, which it definitely isn't anywhere near right now, it won't be on the critical path. |
Currently, the workflow for the tutorial page is:
tutorial.v
Since the tutorial is public-facing and we've gotten a few edits already from people other than me, I think it would be good if the "generate HTML" step happened automatically when changes to tutorial.v were submitted, e.g. as a github action. This would mean that people's changes get reflected automatically, and our Alectryon version is somewhere everyone can see and replicate.
The text was updated successfully, but these errors were encountered: