r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

chore: update toolchain

main
Henrik Böving 2023-04-16 01:30:21 +02:00
parent b9421b9a12
commit e5b44f1cdf
3 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lake-manifest.json
View File

@ -10,7 +10,7 @@
{"git": {"git":
{"url": "https://github.com/leanprover/lake", {"url": "https://github.com/leanprover/lake",
"subDir?": null, "subDir?": null,
"rev": "9e00151251d3e550f1ef4b24e59fd0d0419b0602", "rev": "f120dbcaf8dafe864a5a4c28b34500352dbf1e60",
"name": "lake", "name": "lake",
"inputRev?": "master"}}, "inputRev?": "master"}},
{"git": {"git":
@ -28,6 +28,6 @@
{"git": {"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic", {"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null, "subDir?": null,
"rev": "0930d561409bc8b36551b22e85575009289e602e", "rev": "be1f061688faa1dbb224773c54901661253fb4b8",
"name": "UnicodeBasic", "name": "UnicodeBasic",
"inputRev?": "main"}}]} "inputRev?": "main"}}]}

2
lakefile.lean
View File

@ -71,7 +71,7 @@ library_facet docs (lib) : FilePath := do
-- XXX: Workaround remove later -- XXX: Workaround remove later
let coreJob ← if h : docGen4Pkg.name = _package.name then let coreJob ← if h : docGen4Pkg.name = _package.name then
have : Fact (docGen4Pkg.name = _package.name) := Fact.mk h have : PackageName docGen4Pkg _package.name := ⟨h⟩
let job := fetch <| docGen4Pkg.target `coreDocs let job := fetch <| docGen4Pkg.target `coreDocs
job job
else else

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:nightly-2023-03-15 leanprover/lean4:nightly-2023-04-11