diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index b334824d652c..01d486d79ed7 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -1465,7 +1465,7 @@ def setupEditedModule importArts := transImpArts dynlibs := dynlibs.map (·.path) plugins := plugins.map (·.path) - options := mod.leanOptions + options := mod.serverOptions } /-- diff --git a/tests/lake/tests/setupFile/moreServerOptions.toml b/tests/lake/tests/setupFile/moreServerOptions.toml new file mode 100644 index 000000000000..e82c21c56913 --- /dev/null +++ b/tests/lake/tests/setupFile/moreServerOptions.toml @@ -0,0 +1,7 @@ +name = "test" + +[moreServerOptions] +weak.foo = "baz" + +[[lean_lib]] +name = "Test" diff --git a/tests/lake/tests/setupFile/test.sh b/tests/lake/tests/setupFile/test.sh index d6f75e9c8428..a88ec8ac72d0 100755 --- a/tests/lake/tests/setupFile/test.sh +++ b/tests/lake/tests/setupFile/test.sh @@ -33,6 +33,12 @@ test_out '"options":{}' setup-file ImportFoo.lean # Lake can identify the module corresponding to the path. test_out '"options":{"weak.foo":"bar"}' setup-file Test.lean +# Test that `moreServerOptions` applies to external modules. +test_out '"options":{"weak.foo":"baz"}' -f moreServerOptions.toml setup-file ImportTest.lean + +# Test that `moreServerOptions` applies to internal modules. +test_out '"options":{"weak.foo":"baz"}' -f moreServerOptions.toml setup-file Test.lean + # Test that `setup-file` on an invalid Lean configuration file succeeds. test_run -f invalid.lean setup-file invalid.lean