fix oneshot setup

leanprover-community · Nov 21, 2024 · 375a0a4 · 375a0a4
1 parent 1826bb7
commit 375a0a4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Oneshot/lean4-in/lake-manifest.json b/Oneshot/lean4-in/lake-manifest.json
@@ -18,7 +18,7 @@
    "manifestFile": "lake-manifest.json",
    "inherited": false,
    "dir": "./../../.lake/packages/aesop",
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"type": "path",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
@@ -30,7 +30,7 @@
    "manifestFile": "lake-manifest.json",
    "inherited": false,
    "dir": "./../../.lake/packages/importGraph",
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"type": "path",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",