diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 103c4f81aa..55a7d1cbc8 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -103,11 +103,22 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
         fileName := inputCtx.fileName
         fileMap  := inputCtx.fileMap
       }
-    EIO.toIO ioErrorFromEmpty $
-      Elab.Command.catchExceptions
-        (Elab.Command.elabCommand cmdStx)
-        cmdCtx cmdStateRef
-    let postCmdState ← cmdStateRef.get
+    let (output, _) ← IO.FS.withIsolatedStreams do
+      EIO.toIO ioErrorFromEmpty do
+        Elab.Command.catchExceptions
+          (Elab.Command.elabCommand cmdStx)
+          cmdCtx cmdStateRef
+    let mut postCmdState ← cmdStateRef.get
+    if !output.isEmpty then
+      postCmdState := {
+        postCmdState with
+        messages := postCmdState.messages.add {
+          fileName := inputCtx.fileName
+          severity := MessageSeverity.information
+          pos      := inputCtx.fileMap.toPosition snap.endPos
+          data     := output
+        }
+      }
     let postCmdSnap : Snapshot := {
         beginPos := cmdPos
         stx := cmdStx
diff --git a/tests/lean/interactive/stdOutput.lean b/tests/lean/interactive/stdOutput.lean
new file mode 100644
index 0000000000..856a63b589
--- /dev/null
+++ b/tests/lean/interactive/stdOutput.lean
@@ -0,0 +1,5 @@
+import Lean
+
+elab "foo" : command => IO.println "hi"
+#eval "ho"
+foo
diff --git a/tests/lean/interactive/stdOutput.lean.expected.out b/tests/lean/interactive/stdOutput.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2