Skip to content

Commit

Permalink
bump to nightly-2023-05-06-01
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-bot committed May 6, 2023
1 parent 51185b9 commit 493cc19
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@
[{"git":
{"url": "https://github.com/leanprover-community/lean3port.git",
"subDir?": null,
"rev": "4ae2fa2c01314574d49deb45efe1d9f4c9ae49c1",
"rev": "1039149424af18a477c79d0015cf081147a3ce97",
"name": "lean3port",
"inputRev?": "4ae2fa2c01314574d49deb45efe1d9f4c9ae49c1"}},
"inputRev?": "1039149424af18a477c79d0015cf081147a3ce97"}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
Expand Down
4 changes: 2 additions & 2 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ open Lake DSL System
-- Usually the `tag` will be of the form `nightly-2021-11-22`.
-- If you would like to use an artifact from a PR build,
-- it will be of the form `pr-branchname-sha`.
def tag : String := "nightly-2023-05-05-22"
def tag : String := "nightly-2023-05-06-01"
def releaseRepo : String := "leanprover-community/mathport"
def oleanTarName : String := "mathlib3-binport.tar.gz"

Expand Down Expand Up @@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
untarReleaseArtifact releaseRepo tag oleanTarName libDir
return .nil

require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"4ae2fa2c01314574d49deb45efe1d9f4c9ae49c1"
require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"1039149424af18a477c79d0015cf081147a3ce97"

@[default_target]
lean_lib Mathbin where
Expand Down

0 comments on commit 493cc19

Please sign in to comment.