implies

leanprover-community · Aug 30, 2024 · 3c90f51 · 3c90f51
1 parent 6dc33a1
commit 3c90f51
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
@@ -77,7 +77,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
     let toModule := ImportGraph.getModule to
     let includeLean := args.hasFlag "include-lean"
     let includeStd := args.hasFlag "include-std" || includeLean
-    let includeDeps := args.hasFlag "include-deps" || includeStd
+    let includeDeps := args.hasFlag "include-deps" || args.hasFlag "mark-module" || includeStd
     let filter (n : Name) : Bool :=
       toModule.isPrefixOf n ||
       bif isPrefixOf `Std n then includeStd else

diff --git a/Main.lean b/Main.lean
@@ -21,9 +21,9 @@ def graph : Cmd := `[Cli|
     "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 libraries (not including Lean itself and `std`)"
-    "mark-module";        "visually highlight the current module. Only sensible in combination with `--include-deps`"
-    "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')"
+    "mark-module";        "Visually highlight the current module. (implies `--include-deps`)"
+    "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`)"
 
   ARGS:
     ...outputs : String;  "Filename(s) for the output. \