From 3347220e0a8504e1a0cbaf1612cf64f949ecbfec Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 30 Aug 2024 10:36:01 +1000 Subject: [PATCH] Update Main.lean Co-authored-by: Jon Eugster --- Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index abcf1f0..45ebfff 100644 --- a/Main.lean +++ b/Main.lean @@ -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')"