Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This has been causing warnings all over the place, just because it was a marker variant that was currently not in use. As no markers will be added any more as per the deprecation note, this can go already.
- Loading branch information