Really follow leanprover-community/batteries#446

leanprover-community · Dec 13, 2023 · e8f8e86 · e8f8e86
1 parent 0c2d077
commit e8f8e86
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,13 +1,13 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/nomeata/std4",
    "type": "git",
    "subDir": null,
-   "rev": "483fd2846f9fe5107011ece0cc3d8d88af1a8603",
+   "rev": "1020a8d965b8177e7d73d4c54d36a428ced60827",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "lean-pr-testing-3040",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",

diff --git a/lakefile.lean b/lakefile.lean
@@ -26,7 +26,7 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/nomeata/std4" @ "lean-testing-pr-3040"
+require std from git "https://github.com/nomeata/std4" @ "lean-pr-testing-3040"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23"