From 50b0f4db1f3e384a94f589ed36d24e509904d205 Mon Sep 17 00:00:00 2001 From: acmepjz Date: Sat, 15 Jun 2024 05:06:59 +0800 Subject: [PATCH] chore: update md4lean version and README that it compiles on Windows --- README.md | 3 +-- lake-manifest.json | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 6169c078..dbfe4d82 100644 --- a/README.md +++ b/README.md @@ -35,8 +35,7 @@ need to serve them from a proper http server for it to work. An easy way to do t ## Requirements to run `doc-gen4` In order to compile itself `doc-gen4` requires: - a Lean 4 or `elan` installation -- a C compiler -- being on a Linux or MacOS machine (other operating systems, including Windows, are not tested) +- a C compiler if on Linux or MacOS (on Windows it will use Lean's built-in clang compiler) Apart from this the only requirement for `lake -Kenv=dev build Test:docs` to work is that your target library builds, that is `lake build Test` exits without an error. If this requirement diff --git a/lake-manifest.json b/lake-manifest.json index 0e89089d..4f478e95 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, - "rev": "d812b96744f9b60879cbfa9c436de2b95003db2a", + "rev": "9148a0a7506099963925cf239c491fcda5ed0044", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main",