Skip to content

Commit

Permalink
missed a spot
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 committed Aug 18, 2021
1 parent 14be067 commit 72d6942
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,3 +37,4 @@ import Mathlib.Tactic.Split
import Mathlib.Tactic.Spread
import Mathlib.Tactic.SudoSetOption
import Mathlib.Util.Export
import Mathlib.Util.Time

0 comments on commit 72d6942

Please sign in to comment.