diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 81575ed3..f8e70a59 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -19,8 +19,9 @@ def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
+  let oldMessages := commandState.messages.toList
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  pure (s, oldMessages ++ s.messages.toList, s.infoState.trees.toList)
 
 /--
 Process some text input, with or without an existing command state.