From 7ba21c4d1bca70637a9aaa78fef6424588a1d0f6 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Tue, 16 Dec 2025 18:30:01 +0100
Subject: [PATCH] fix: incorrect `inherit_doc` (#11704)

This PR fixes an incorrect `inherit_doc` in `Init.System.IO`.
---
 src/Init/System/IO.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 6d6b1ddb83..20261fcece 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -196,7 +196,7 @@ causing the side effect to occur at initialization time, even if it would otherw
 @[inline] unsafe def unsafeEIO (fn : EIO ε α) : Except ε α :=
   unsafeBaseIO fn.toBaseIO
 
-@[inline, inherit_doc EIO] unsafe def unsafeIO (fn : IO α) : Except IO.Error α :=
+@[inline, inherit_doc unsafeEIO] unsafe def unsafeIO (fn : IO α) : Except IO.Error α :=
   unsafeEIO fn