Skip to content

Commit 21893cf

Browse files
committed
chore: remove offset option
1 parent d524bc1 commit 21893cf

File tree

1 file changed

+0
-5
lines changed

1 file changed

+0
-5
lines changed

src/Init/Grind/Config.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -153,11 +153,6 @@ structure Config where
153153
at least `Std.IsPreorder`
154154
-/
155155
order := true
156-
/--
157-
When `true` (default: `true`), enables the legacy module `offset`. This module will be deleted in
158-
the future.
159-
-/
160-
offset := true
161156
deriving Inhabited, BEq
162157

163158
/--

0 commit comments

Comments
 (0)