style

leanprover-community · Sep 3, 2024 · 16fcfe0 · 16fcfe0
1 parent 14a8466
commit 16fcfe0
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
@@ -86,7 +86,9 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
     let includeLean := args.hasFlag "include-lean"
     let includeStd := args.hasFlag "include-std" || includeLean
     let includeDeps := args.hasFlag "include-deps" || includeStd
-    -- `includeDirect` does not imply `includeDeps`, e.g. `import Lean`.
+    -- Note: `includeDirect` does not imply `includeDeps`!
+    -- e.g. if the module contains `import Lean`, the node `Lean` will be included with
+    -- `--include-direct`, but not included with `--include-deps`.
     let includeDirect := args.hasFlag "include-direct"
 
     -- `directDeps` contains files which are not in the module