From f57a9186f63460e2b4063692dcdfe262d320d841 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 2 Sep 2024 11:39:49 +0200
Subject: [PATCH] add comment
---
ImportGraph/Cli.lean | 1 +
1 file changed, 1 insertion(+)
diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean
index 6a47129..802822d 100644
--- a/ImportGraph/Cli.lean
+++ b/ImportGraph/Cli.lean
@@ -84,6 +84,7 @@ 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
+ -- `includeDirectDeps` does not imply `includeDeps`, e.g. `import Lean`.
let includeDirectDeps := args.hasFlag "include-direct-deps"
-- If the flag is set, `directDeps` contains files which are not in the module