README

leanprover-community · Oct 29, 2024 · fa418ca · fa418ca
1 parent fe586e6
commit fa418ca
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/ImportGraph.lean b/ImportGraph.lean
@@ -3,3 +3,4 @@ import ImportGraph.Imports
 import ImportGraph.CurrentModule
 import ImportGraph.Lean.Name
 import ImportGraph.RequiredModules
+import ImportGraph.UnusedTransitiveImports
diff --git a/README.md b/README.md
@@ -24,6 +24,11 @@ lake exe graph --to MyModule my_graph.pdf
 ```
 where `MyModule` follows the same module naming you would use to `import` it in lean. See `lake exe graph --help` for more options.
 
+You can specify multiple sources and targets e.g. as
+```bash
+lake exe graph --from MyModule1,MyModule2 --to MyModule3,MyModule4 my_graph.pdf
+```
+
 ### Troubleshoot
 
 * make sure to `lake build` your project (or the specified `--to` module) before using `lake exe graph`!