From ee4dc452ac09835bcdfe54d54941e5e72f601760 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Sep 2020 16:10:29 -0700
Subject: [PATCH] chore: remove leftover

---
 src/Lean/Parser/Do.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 3a3d34ec7a..fdf9c30793 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -78,9 +78,7 @@ withPosition fun pos₁ =>
     ("; "
      -- check indentation
      >> checkColGe pos₁.column "do-elements must be indented"
-     -- no black lines between do-elements.
-     -- >> checkLineLe (pos₂.line+1) "no blank lines between do-elements"
-      >> notFollowedByCommandToken)
+     >> notFollowedByCommandToken)
   >> optional (try ("; " >> notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)))
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
 def doSeq          := doSeqBracketed <|> doSeqIndent