Skip to content

Commit 2fc2287

Browse files
committed
restore option as no-op to not break the world
1 parent bf46c31 commit 2fc2287

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/Lean/Language/Lean.lean

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -355,6 +355,11 @@ private def getNiceCommandStartPos? (stx : Syntax) : Option String.Pos.Raw := do
355355
stx := stx[1]
356356
stx.getPos?
357357

358+
register_builtin_option experimental.module : Bool := {
359+
defValue := false
360+
descr := "no-op, deprecated"
361+
}
362+
358363
/--
359364
Entry point of the Lean language processor.
360365

0 commit comments

Comments
 (0)