Workflow alignment #282
Labels
enhancement
New feature or request
good first issue
Good for newcomers
help wanted
Extra attention is needed
Work-in-progress
Currently being worked on, not ready for merge.
It's preferable to align the workflows of HepLean with that of Mathlib. Here's the task breakdown:
doclean
directory as suggested by doc-gen4, and create a workflow that is triggered when a PR merges similar to the documentation generation of Mathlib barring the separate repo. This preventslake
, called from the top-level, from pulling and building doc-gen4 and its dependencies.If more tasks are required, feel free to add them to the list above, and link related PRs to the "Development" section on the right of the GitHub web UI.
The text was updated successfully, but these errors were encountered: