From efd52f67c3c102d0fd45cfd06f66fca65a43190b Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Tue, 12 Sep 2023 00:28:04 -0400
Subject: [PATCH] chore: clean up test file formatting

---
 test/tryThis.lean | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/test/tryThis.lean b/test/tryThis.lean
index ebde171a1a..890babf607 100644
--- a/test/tryThis.lean
+++ b/test/tryThis.lean
@@ -43,13 +43,13 @@ elab "add_suggestions" s:term "with_header" h:term : tactic => unsafe do
 
 /-- Demo adding a suggestion. -/
 macro "#demo1" s:term : command => `(example : True := by add_suggestion $s; trivial)
-/--Demo adding a suggestion with a header. -/
+/-- Demo adding a suggestion with a header. -/
 macro "#demo1" s:term "with_header" h:term : command => `(example : True := by
   add_suggestion $s with_header $h; trivial)
-/--Demo adding suggestions. -/
+/-- Demo adding suggestions. -/
 macro "#demo" s:term : command => `(example : True := by
   add_suggestions $s; trivial)
-/--Demo adding suggestions with a header. -/
+/-- Demo adding suggestions with a header. -/
 macro "#demo" s:term "with_header" h:term : command => `(example : True := by
   add_suggestions $s with_header $h; trivial)
 
@@ -114,19 +114,21 @@ Try these:
 -- `Try this: rfl` -- styled like an inaccessible goal hypothesis
 #demo1 {s with style? := some .asInaccessible}
 
-/--info: Try this: rfl-/
+/-- info: Try this: rfl -/
 #guard_msgs in
 -- `Try this: Starfleet`
 #demo1 {s with preInfo? := "Sta", postInfo? := "eet"}
 
-/--info: Try this: a secret message-/
+/-- info: Try this: a secret message -/
 #guard_msgs in
 -- `Try this: rfl`
 #demo1 {s with messageData? := m!"a secret message"}
 
-/--info: Try these:
+/--
+info: Try these:
 • a secret message
-• another secret message-/
+• another secret message
+-/
 #guard_msgs in
 -- `Try this: rfl`
 #demo #[
@@ -134,15 +136,17 @@ Try these:
   {s with messageData? := m!"another secret message"}
 ]
 
-/--info: Our only hope is rfl-/
+/-- info: Our only hope is rfl -/
 #guard_msgs in
 #demo1 s with_header "Our only hope is "
 
-/--info: We've got everything here! Such as:
+/--
+info: We've got everything here! Such as:
+• rfl
 • rfl
 • rfl
 • rfl
-• rfl-/
+-/
 #guard_msgs in
 #demo #[s,s,s,s] with_header "We've got everything here! Such as:"