From 225e08965d644715e8961cd205ffedf1cf7d24c2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 14 Oct 2024 12:29:03 +1100
Subject: [PATCH] chore: import orphaned Lean.Replay (#5693)

As noticed on
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Reverse.20FFI.20undefined.20reference.20for.20mathlib/near/475824204).
---
 src/Lean.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean.lean b/src/Lean.lean
index dd3eccd7e9..bcd0979df1 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -37,3 +37,4 @@ import Lean.Linter
 import Lean.SubExpr
 import Lean.LabelAttribute
 import Lean.AddDecl
+import Lean.Replay