diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 5964e6b29d..8f8ab49def 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -382,7 +382,9 @@ def toggleInsideQuot.formatter (p : Formatter) : Formatter :=
 p
 
 @[combinatorFormatter checkWsBefore] def checkWsBefore.formatter : Formatter := do
-pushLine
+st ← get;
+when (st.leadWord != "") $
+  pushLine
 
 @[combinatorFormatter checkPrec] def checkPrec.formatter : Formatter := pure ()
 @[combinatorFormatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
index 244e3122a9..225a75679c 100644
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -10,7 +10,7 @@ precissues.lean:17:10: error: expected command, but found term; this error may b
 1 : Nat
 id ((fun (this : True) => this) True.intro) : True
 0 = (fun (this : Nat) => this) 1 : Prop
-0 = let x  : Nat := 0;
+0 = let x : Nat := 0;
   x : Prop
 p ↔ ¬q : Prop
 True = ¬False : Prop