diff --git a/lake-manifest.json b/lake-manifest.json
index 9e301c0..4586840 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,11 +15,21 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
+   "rev": "47f0ce028df42a72dc5d55e40bd4c1921a7f98bd",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v1.3.0",
+   "inputRev": "1.11.0",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "«lean4-metaprogramming-book»",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index c1b174a..d9a4125 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,7 +10,7 @@ lean_lib «lean4-metaprogramming-book» where
   globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions]
 
 require mdgen from git
-  "https://github.com/Seasawher/mdgen" @ "v1.3.0"
+  "https://github.com/Seasawher/mdgen" @ "1.11.0"
 
 require "leanprover-community" / "batteries" @ git "main"
 
diff --git a/lean/main/01_intro.lean b/lean/main/01_intro.lean
index 640e7b8..fb6cfa1 100644
--- a/lean/main/01_intro.lean
+++ b/lean/main/01_intro.lean
@@ -128,14 +128,14 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
       logInfo "success"
     catch | _ => throwError "failure"
 
-/-- info: success -/
+/-⋆-//-- info: success -/
 #guard_msgs in --#
 #assertType 5 : Nat
 
 -- don't display names of metavariables
 set_option pp.mvars false in
 
-/--
+/-⋆-//--
 error: type mismatch
   []
 has type
diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean
index 5cd7a1a..0814f5e 100644
--- a/lean/main/09_tactics.lean
+++ b/lean/main/09_tactics.lean
@@ -39,7 +39,7 @@ We start by simply declaring the tactic with no implementation:
 
 syntax "custom_tactic" : tactic
 
-/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
+/-⋆-//-- error: tactic 'tacticCustom_tactic' has not been implemented -/
 #guard_msgs in --#
 example : 42 = 42 := by
   custom_tactic
diff --git a/lean/solutions/05_syntax.lean b/lean/solutions/05_syntax.lean
index 2c5cba2..ee0faf1 100644
--- a/lean/solutions/05_syntax.lean
+++ b/lean/solutions/05_syntax.lean
@@ -36,11 +36,11 @@ syntax "yellow" : tactic
 
 #check_failure good morning -- the syntax parsing stage works
 
-/-- error: elaboration function for 'commandHello' has not been implemented -/
+/-⋆-//-- error: elaboration function for 'commandHello' has not been implemented -/
 #guard_msgs in --#
 hello -- the syntax parsing stage works
 
-/-- error: tactic 'tacticYellow' has not been implemented -/
+/-⋆-//-- error: tactic 'tacticYellow' has not been implemented -/
 #guard_msgs in --#
 example : 2 + 2 = 4 := by
   yellow -- the syntax parsing stage works