diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 0f1468e..a769148 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -1,7 +1,7 @@ import CMark import DocGen4.Output.Template import Lean.Data.Parsec -import UnicodeData +import UnicodeBasic open Lean Xml Parser Parsec DocGen4.Process diff --git a/lake-manifest.json b/lake-manifest.json index 9c8bded..26301a3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -26,8 +26,8 @@ "name": "leanInk", "inputRev?": "doc-gen"}}, {"git": - {"url": "https://github.com/fgdorais/UnicodeData", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "subDir?": null, - "rev": "fb9efcfc2b832c2aff45a220779f35b79f62da11", - "name": "UnicodeData", + "rev": "4653d015b3ebd3d7980886a4daa75722d1d4e518", + "name": "UnicodeBasic", "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index a718390..d1d53d2 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,8 +14,8 @@ lean_exe «doc-gen4» { require CMark from git "https://github.com/xubaiw/CMark.lean" @ "main" -require UnicodeData from git - "https://github.com/fgdorais/UnicodeData" @ "main" +require UnicodeBasic from git + "https://github.com/fgdorais/lean4-unicode-basic" @ "main" require Cli from git "https://github.com/mhuisi/lean4-cli" @ "nightly"