From 16fcfe0fb83114810b1067579d4f8d69a2ddb1f6 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 3 Sep 2024 15:01:21 +0200 Subject: [PATCH] style --- ImportGraph/Cli.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ImportGraph/Cli.lean b/ImportGraph/Cli.lean index bbbbf86..b4ab70d 100644 --- 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