docs: fix a test description

thorimur · Oct 24, 2023 · 640753d · 640753d
1 parent 0d39f21
commit 640753d
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/test/tryThis.lean b/test/tryThis.lean
@@ -163,7 +163,13 @@ info: Try these:
 • another secret message
 -/
 #guard_msgs in
--- `Try this: rfl`
+/-
+```
+Try these:
+• rfl
+• rfl
+```
+-/
 #demo #[
   {s with messageData? := m!"a secret message"},
   {s with messageData? := m!"another secret message"}