chore: use upstream version of MD4Lean

The Verso-specific features have been upstreamed.
leanprover · Jan 17, 2025 · 481a79b · 481a79b
1 parent 2482378
commit 481a79b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,14 +1,14 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/david-christiansen/md4lean",
+ [{"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6f0beb756af7de9ebd0bf38044bc9ac34419cacd",
+   "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "parser",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/subverso.git",

diff --git a/lakefile.lean b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 require subverso from git "https://github.com/leanprover/subverso.git"@"main"
-require MD4Lean from git "https://github.com/david-christiansen/md4lean"@"parser"
+require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 
 package verso where
   precompileModules := true