Skip to content
GitLab

move coPset-generic hint to coPset.v

Merged Ralf Jung requested to merge ralf/hints into master

I see no good reason for it to be in namespaces.v. The old one that got removed in e09f7ce3 was in coPset.v as well.

Merge request reports