From cc7b780d23b2cdff372f9e71373d262571216535 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 5 May 2023 13:11:17 -0600 Subject: [PATCH] Update bookshelf-docgen to version with HTML copying support. --- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 1088b4c..292612f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -16,9 +16,9 @@ {"git": {"url": "https://github.com/jrpotter/bookshelf-docgen.git", "subDir?": null, - "rev": "8e2df427700e42610ddb51137698a105555d381d", + "rev": "1333269547cdd3f297cf9097fb124ae7c413dd00", "name": "doc-gen4", - "inputRev?": "8e2df427700e42610ddb51137698a105555d381d"}}, + "inputRev?": "1333269547cdd3f297cf9097fb124ae7c413dd00"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, @@ -52,7 +52,7 @@ {"git": {"url": "https://github.com/fgdorais/lean4-unicode-basic", "subDir?": null, - "rev": "ce508dcd1fd49ba15675861aafd864572a0b8252", + "rev": "be1f061688faa1dbb224773c54901661253fb4b8", "name": "UnicodeBasic", "inputRev?": "main"}}, {"git": diff --git a/lakefile.lean b/lakefile.lean index f66e9f4..dee9644 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,7 @@ require std4 from git "6006307d2ceb8743fea7e00ba0036af8654d0347" require «doc-gen4» from git "https://github.com/jrpotter/bookshelf-docgen.git" @ - "8e2df427700e42610ddb51137698a105555d381d" + "1333269547cdd3f297cf9097fb124ae7c413dd00" @[default_target] lean_lib «Bookshelf» {