Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
ci: run full pipeline on docs-only changes (#913)
This is technically more heavy than necessary, but I think changes that only touch docs won't be too frequent and it's better than no CI at all on those PRs. Fixes #796.
- Loading branch information