aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh
AgeCommit message (Collapse)Author
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion