Skip to content

Commit

Permalink
maybe this import should go?
Browse files Browse the repository at this point in the history
  • Loading branch information
jcommelin committed Nov 11, 2024
1 parent ebcdcf2 commit f0a1ccc
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion ImportGraph.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,3 @@ import ImportGraph.Imports
import ImportGraph.CurrentModule
import ImportGraph.Lean.Name
import ImportGraph.RequiredModules
import ImportGraph.UnusedTransitiveImports

0 comments on commit f0a1ccc

Please sign in to comment.