Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Jon Eugster <[email protected]>
  • Loading branch information
kim-em and joneugster authored Oct 30, 2024
1 parent fa418ca commit 5c04dea
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ def graph : Cmd := `[Cli|

FLAGS:
"show-transitive"; "Show transitively redundant edges."
"to" : Array ModuleName; "Only show the upstream imports of the specified module."
"from" : Array ModuleName; "Only show the downstream dependencies of the specified module."
"to" : Array ModuleName; "Only show the upstream imports of the specified modules."
"from" : Array ModuleName; "Only show the downstream dependencies of the specified modules."
"exclude-meta"; "Exclude any files starting with `Mathlib.[Tactic|Lean|Util|Mathport]`."
"include-direct"; "Include directly imported files from other libraries"
"include-deps"; "Include used files from other libraries (not including Lean itself and `std`)"
Expand Down

0 comments on commit 5c04dea

Please sign in to comment.