diff options
Diffstat (limited to 'math/lean4/files/patch-tests_lakefile.toml')
| -rw-r--r-- | math/lean4/files/patch-tests_lakefile.toml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/math/lean4/files/patch-tests_lakefile.toml b/math/lean4/files/patch-tests_lakefile.toml new file mode 100644 index 000000000000..3a01b013943d --- /dev/null +++ b/math/lean4/files/patch-tests_lakefile.toml @@ -0,0 +1,10 @@ +--- tests/lakefile.toml.orig 2025-11-17 18:29:21 UTC ++++ tests/lakefile.toml +@@ -1,5 +1,7 @@ + name = "tests" + ++weakLeancArgs = ["-fPIC"] ++ + # Allow `module` in tests when opened in the language server. + # Enabled during actual test runs in the respective test_single.sh. + moreGlobalServerArgs = ["-Dexperimental.module=true"] |