From bc38caf177768a491fa05646ccd7e2c5d1829f28 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Wed, 24 Jan 2024 22:38:38 +0000
Subject: [PATCH] update lakefile to undeprecated moreServerOptions

---
 lakefile.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index bbbd889..6857589 100644
--- 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]