Skip to content

Commit

Permalink
add comment
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Sep 2, 2024
1 parent b87256b commit f57a918
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions ImportGraph/Cli.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit f57a918

Please sign in to comment.