From 5c7cf765758044dd34f68c24c574ddd07175073e Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Fri, 7 Oct 2022 11:17:17 -0400 Subject: [PATCH] doc: fix link to initialization section in ffi section The current link goes to doc/dev#init, where there is nothing about initialization. This PR fixes the link so that it points to the initialization section lower down on the ffi page. --- doc/dev/ffi.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/dev/ffi.md b/doc/dev/ffi.md index 3e92abd2e4..0f0dd66723 100644 --- a/doc/dev/ffi.md +++ b/doc/dev/ffi.md @@ -21,7 +21,7 @@ If `n` is 0, the corresponding C declaration is extern s sym; ``` where `s` is the C translation of `β` as specified in the next section. -In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](.#init). +In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](#initialization). If `n` is greater than 0, the corresponding C declaration is ```c