Skip to content

[Merged by Bors] - feat(init/meta/interative): Change the behaviour of specialize to put goals from underscores first#530

Closed
shingtaklam1324 wants to merge 2 commits intoleanprover-community:masterfrom shingtaklam1324:patch-3

Commits

Commits on Feb 11, 2021