doc: clarify that lean_initialize_runtime_module is implied by `lea…

…n_initialize`
leanprover · Jan 17, 2025 · f10162f · f10162f
1 parent e3fd954
commit f10162f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/doc/dev/ffi.md b/doc/dev/ffi.md
@@ -140,7 +140,7 @@ lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
 lean_initialize_runtime_module();
-//lean_initialize();  // necessary if you (indirectly) access the `Lean` package
+//lean_initialize();  // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package
 
 lean_object * res;
 // use same default as for Lean executables