update lakefile to undeprecated moreServerOptions

2024-01-24 22:38:38 +00:00
parent 923c4fb175
commit bc38caf177
1 changed files with 4 additions and 4 deletions
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -46,10 +46,10 @@ package Game where
    "-Dtactic.hygienic=false",
    "-Dlinter.unusedVariables.funArgs=false",
    "-Dtrace.debug=false"]
-  moreServerArgs := #[
-    "-Dtactic.hygienic=false",
-    "-Dlinter.unusedVariables.funArgs=true",
-    "-Dtrace.debug=true"]
+  moreServerOptions := #[
+    ⟨`tactic.hygienic, false⟩,
+    ⟨`linter.unusedVariables.funArgs, true⟩,
+    ⟨`trace.debug, true⟩]
  weakLeanArgs := #[]

@[default_target]