chore: missing LEAN_EXPORT

tydeu · tydeu · commit 1ef7092a8f35 · 2025-12-01T16:24:14.000+01:00
diff --git a/src/util/options.cpp b/src/util/options.cpp
@@ -52,12 +52,12 @@ bool get_verbose(options const & opts) {
 }
 
 /* getDefaultVerbose (_ : Unit) : Bool */
-extern "C" uint8 lean_internal_get_default_verbose(obj_arg) {
+extern "C" LEAN_EXPORT uint8 lean_internal_get_default_verbose(obj_arg) {
     return LEAN_DEFAULT_VERBOSE;
 }
 
 /* getDefaultOptions (_ : Unit) : Options */
-extern "C" obj_res lean_internal_get_default_options(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_internal_get_default_options(obj_arg) {
     return get_default_options().steal();
 }
 

Original file line number	Diff line number	Diff line change
`@@ -52,12 +52,12 @@ bool get_verbose(options const & opts) {`
`52`	`52`	`}`
`53`	`53`
`54`	`54`	`/* getDefaultVerbose (_ : Unit) : Bool */`
`55`		`-extern "C" uint8 lean_internal_get_default_verbose(obj_arg) {`
	`55`	`+extern "C" LEAN_EXPORT uint8 lean_internal_get_default_verbose(obj_arg) {`
`56`	`56`	`return LEAN_DEFAULT_VERBOSE;`
`57`	`57`	`}`
`58`	`58`
`59`	`59`	`/* getDefaultOptions (_ : Unit) : Options */`
`60`		`-extern "C" obj_res lean_internal_get_default_options(obj_arg) {`
	`60`	`+extern "C" LEAN_EXPORT obj_res lean_internal_get_default_options(obj_arg) {`
`61`	`61`	`return get_default_options().steal();`
`62`	`62`	`}`
`63`	`63`