diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 648a253..55bced3 100644 --- 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."