Skip to content

Remove the `*` specialization pattern.

Robbert Krebbers requested to merge robbert/remove_star_spec_pattern into master

This pattern has been deprecated and a no-op since 2017. See !41 (merged).

Merge request reports