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

fix: unicode dependency

main
F. G. Dorais 2023-03-14 07:32:32 -04:00 committed by Henrik Böving
parent 0c415232cd
commit 5ab7d0bdd8
3 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Output/DocString.lean
View File

@ -1,7 +1,7 @@
import CMark import CMark
import DocGen4.Output.Template import DocGen4.Output.Template
import Lean.Data.Parsec import Lean.Data.Parsec
import UnicodeData import UnicodeBasic
open Lean Xml Parser Parsec DocGen4.Process open Lean Xml Parser Parsec DocGen4.Process

6
lake-manifest.json
View File

@ -26,8 +26,8 @@
"name": "leanInk", "name": "leanInk",
"inputRev?": "doc-gen"}}, "inputRev?": "doc-gen"}},
{"git": {"git":
{"url": "https://github.com/fgdorais/UnicodeData", {"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null, "subDir?": null,
"rev": "fb9efcfc2b832c2aff45a220779f35b79f62da11", "rev": "4653d015b3ebd3d7980886a4daa75722d1d4e518",
"name": "UnicodeData", "name": "UnicodeBasic",
"inputRev?": "main"}}]} "inputRev?": "main"}}]}

4
lakefile.lean
View File

@ -14,8 +14,8 @@ lean_exe «doc-gen4» {
require CMark from git require CMark from git
"https://github.com/xubaiw/CMark.lean" @ "main" "https://github.com/xubaiw/CMark.lean" @ "main"
require UnicodeData from git require UnicodeBasic from git
"https://github.com/fgdorais/UnicodeData" @ "main" "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
require Cli from git require Cli from git
"https://github.com/mhuisi/lean4-cli" @ "nightly" "https://github.com/mhuisi/lean4-cli" @ "nightly"