Skip to content

Commit

Permalink
Update Main.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
  • Loading branch information
kim-em and joneugster authored Aug 30, 2024
1 parent d8b01ef commit 3347220
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ def graph : Cmd := `[Cli|
to : ModuleName; "Only show the upstream imports of the specified module."
"from" : ModuleName; "Only show the downstream dependencies of the specified module."
"exclude-meta"; "Exclude any files starting with `Mathlib.[Tactic|Lean|Util|Mathport]`."
"include-deps"; "Include used files from other projects (e.g. lake packages)"
"include-deps"; "Include used files from other libraries (not including Lean itself and `std`)"
"include-std"; "Include used files from the Lean standard library (implies 'include-deps')"
"include-lean"; "Include used files from Lean itself (implies 'include-deps' and 'include-std')"

Expand Down

0 comments on commit 3347220

Please sign in to comment.