Skip to content

Commit

Permalink
chore: test patch for std4#198
Browse files Browse the repository at this point in the history
Remove this commit before merging
  • Loading branch information
fgdorais committed Nov 2, 2023
1 parent 0b8e923 commit 7da3bf9
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 9 deletions.
16 changes: 8 additions & 8 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,6 @@
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "fb43b83c13d10b90299d10d96512d20d33daa658",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/quote4",
"subDir?": null,
"rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
Expand Down Expand Up @@ -40,5 +32,13 @@
"opts": {},
"name": "Cli",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/fgdorais/std4",
"subDir?": null,
"rev": "cea56f69275f6a2ee8e263989cc69498f7a3854b",
"opts": {},
"name": "std",
"inputRev?": "nat-mul",
"inherited": false}}],
"name": "mathlib"}
2 changes: 1 addition & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ lean_exe checkYaml 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/leanprover/std4" @ "main"
require std from git "https://github.com/fgdorais/std4" @ "nat-mul"
require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
Expand Down

0 comments on commit 7da3bf9

Please sign in to comment.