remove logInfo for Branch finishing proof

leanprover-community · Apr 8, 2024 · ce71bc8 · ce71bc8
1 parent 7cedfc5
commit ce71bc8
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
@@ -577,7 +577,8 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
   -- Show an info whether the branch proofs all remaining goals.
   let gs ← Tactic.getUnsolvedGoals
   if gs.isEmpty then
-    trace[debug] "This branch finishes the proof."
+    -- trace[debug] "This branch finishes the proof."
+    pure ()
   else
     trace[debug] "This branch leaves open goals."