Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
.github: remove ensure-docs-compiled workflow
Since the workflow relies on the build-docs target existing in the Makefile to ensure we don't commit a change without calling it, and since we removed it in the previous commit to fold it in generate, we don't need it anymore so we can remove it. Since the `make generate' call is already required if modifying the docs, and we check that during validate, this is safe to remove.
- Loading branch information