Skip to content
This repository has been archived by the owner on Aug 29, 2023. It is now read-only.

chore(import-graph): don't overwrite 'PR' colour with 'ready' colour #133

Merged
merged 2 commits into from Nov 12, 2022

Conversation

semorrison
Copy link
Collaborator

The colours scheme in import-graph makes more sense if the "PR" status takes precedence of the "ready" colour.

@semorrison
Copy link
Collaborator Author

Oh, I hadn't seen #132. This PR is subsumed by that one, although I don't immediately understand what else it is doing!

@joneugster
Copy link

joneugster commented Nov 12, 2022

Please go ahead and merge this PR before #132! I didn't realise it would include any commits I made to my mathlib-tool fork automatically into the PR and used the same fork to do something different.

I might close #132, I use --include-deps locally on a non-mathlib project to show me which imports of mathlib are needed for it to be Lean4-ready. It goes recursively into any dependencies outside the project and includes them into the import-graph, too.

@PatrickMassot PatrickMassot merged commit 8b46291 into master Nov 12, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants