Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix build error introduced by previous commit (#1224)
Note that the `check-index-version` workflow will still fail for this commit because it checks out the previous version of the master, which because of the build error we are fixing here does not compile. Everything should be fine again starting with the next commit after this one.
- Loading branch information