r
/
bookshelf
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Now point to doc-gen4 fork.

main
Joshua Potter 2023-12-14 15:24:10 -07:00
parent 9864ffd7a0
commit f76457cd6f
4 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitmodules vendored Normal file
View File

@ -0,0 +1,3 @@
[submodule "doc-gen4"]
path = doc-gen4
url = git@github.com:jrpotter/bookshelf-doc.git

1
doc-gen4 Submodule

@ -0,0 +1 @@
Subproject commit 86d5c219a9ad7aa686c9e0e704af030e203c63a1

7
lake-manifest.json
View File

@ -82,14 +82,11 @@
"inputRev": "doc-gen", "inputRev": "doc-gen",
"inherited": true, "inherited": true,
"configFile": "lakefile.lean"}, "configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/doc-gen4", {"type": "path",
"type": "git",
"subDir": null,
"rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
"name": "«doc-gen4»", "name": "«doc-gen4»",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false, "inherited": false,
"dir": "././doc-gen4",
"configFile": "lakefile.lean"}], "configFile": "lakefile.lean"}],
"name": "bookshelf", "name": "bookshelf",
"lakeDir": ".lake"} "lakeDir": ".lake"}

3
lakefile.lean
View File

@ -11,8 +11,7 @@ require std from git
"https://github.com/leanprover/std4.git" @ "https://github.com/leanprover/std4.git" @
"v4.3.0" "v4.3.0"
meta if get_config? env = some "dev" then meta if get_config? env = some "dev" then
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ require «doc-gen4» from "./doc-gen4"
"main"
@[default_target] @[default_target]
lean_lib «Bookshelf» { lean_lib «Bookshelf» {