Commit 96d9e88
.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.1 parent 8ac64df commit 96d9e88
1 file changed
Lines changed: 0 additions & 22 deletions
This file was deleted.
0 commit comments