mdgen のバグで #lint コマンドの出力をアサートできていない

Fixes #1230

LeanByExample/Diagnostic/Lint.lean

@@ -21,8 +21,14 @@ info: -- Found 0 errors in 1 declarations
   -- 定理は対象外なのでスルーされる
   #lint only docBlame
 
--- 技術的な理由で `#lint` の出力は省略しているが、
 -- エラーになっている
-#guard_msgs (drop error) in
+/--
+error: -- Found 1 error in 1 declarations (plus 0 automatically generated ones) in the current file with 1 linters
+
+/- The `docBlameThm` linter reports:
+THEOREMS ARE MISSING DOCUMENTATION STRINGS: -/
+#check hoge /- theorem missing documentation string -/
+-/
+#guard_msgs (error) in
   -- ドキュメントコメントのない定理に対して警告するリンタを実行している
   #lint only docBlameThm

lake-manifest.json

@@ -8,14 +8,14 @@
    "rev": "ec10d9ba44225d66e790787d0f5b19a14830337e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "ec10d9ba44225d66e790787d0f5b19a14830337e",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0d7e8b67b1088cb2d51bb2d3f175f9517e5e0fa3",
+   "rev": "ddec7bc2d811777502789c678445b7a47a265baa",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -12,7 +12,7 @@ abbrev linterOptions : Array LeanOption := #[
 ]
 
 package «Lean by Example» where
-  keywords := #["manual", "reference", "tutorial", "japanese", "cheatsheet"]
+  keywords := #["manual", "reference", "japanese"]
   description := "プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。"
   leanOptions := #[
     ⟨`autoImplicit, false⟩,
@@ -24,7 +24,7 @@ require mdgen from git
   "https://github.com/Seasawher/mdgen" @ "main"
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "master"
+  "https://github.com/leanprover-community/mathlib4.git" @ "ec10d9ba44225d66e790787d0f5b19a14830337e"
 
 @[default_target]
 lean_lib LeanByExample where