Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Looking at git history, this was added in #251 and was probably an overzealous add TBH. I often like pinning, but here it's breaking our runs: #507 So let's relax it for now. If we later run into problems, we can always tighten the screws later.
- Loading branch information