Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
PR #332 deprecated after the discussion of issue #315, but it is a measure not yet necessary to take. Revert the deprecation and wait for us to reach a consensus.
- Loading branch information