Def importGraphCLI

Modification history

2024-01-10 11:53
ImportGraph/Main.lean
refactor: split `ImportGraph` into its own package. (#9169) …
Deleted importGraphCLIView on Github →
2023-07-12 04:07
Util/ImportGraph/Main.lean
chore: revert move utilities into Util directory (#5787) (#5825) …
Deleted importGraphCLIView on Github →
2023-07-11 10:52
Util/ImportGraph/Main.lean
chore: move utilities into Util directory (#5787) …
Added importGraphCLIView on Github →
2023-07-10 05:24
ImportGraph/Main.lean
feat: `lake exe graph`, as replacement for `leanproject import-graph` (#5513) …
Added importGraphCLIView on Github →