chore: switch back to main branch of md4lean

leanprover · Jan 5, 2025 · 2c27958 · 2c27958
1 parent 5a111eb
commit 2c27958
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 9 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "51b0cd28a0ca79ccfa91b8c7d5eb94ba075dfdb4",
+   "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,20 +25,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
+   "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/kim-em/md4lean",
+  {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "17e3f60bca8b6fdc19a55e2a7c9840a9f7afd1dc",
+   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bump_to_v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«doc-gen4»",

diff --git a/lakefile.lean b/lakefile.lean
@@ -12,10 +12,7 @@ lean_exe «doc-gen4» {
 }
 
 require MD4Lean from git
-  -- This should be the original version:
-  -- "https://github.com/acmepjz/md4lean" @ "main"
-  -- but as we don't have write access to that repo we are temporarily using this fork:
-  "https://github.com/kim-em/md4lean" @ "bump_to_v4.16.0-rc1"
+  "https://github.com/acmepjz/md4lean" @ "main"
 
 require BibtexQuery from git
   "https://github.com/dupuisf/BibtexQuery" @ "master"