https://github.com/leanprover-community/import-graph/pull/38

Stream: general

[Kim Morrison]

@Jon Eugster, just continuing your comment

@kim-em when adding features I think it would be good if you updated the README (Commands section), too.

from this PR here, as I tend to miss conversations on already closed PRs.

I think in this case the PR did not add any user facing functionality (i.e. lake exe or #shiny_cmd), only internal API, so there is nothing to add to the README.

[Jon Eugster]

I think the PR (link) adds #unused_transitive_imports, doesn't it?

Anyways, partially I commented on this closed PR in order for myself to remember to come back to it later, read the code more carefully and update the docs myself.
Wouldn't have been the end of the world if you'd missed the comment, I know that not everybody is looking at their github notifications :blush: (sometimes because there are simply too many). If it's something important I'd write on Zulip:+1:

[Jon Eugster]

Ah but I see, the command is only added in a test file, didn't spot that, my bad!