From 10a8822ac54ff94f48a2c2454d508fef05b0c4c8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Aug 2019 10:45:15 -0700
Subject: [PATCH] fix(library/init/lean/parser/module): use `updateLeading`

---
 library/init/lean/parser/module.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean
index a36b2f08c8..167d8c2bf0 100644
--- a/library/init/lean/parser/module.lean
+++ b/library/init/lean/parser/module.lean
@@ -111,7 +111,8 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
   | (stx, state, msgs) =>
     if isEOI stx then
       if msgs.isEmpty then
-        pure (mkListNode stxs)
+        let stx := mkListNode stxs;
+        pure stx.updateLeading
       else do
         msgs.toList.mfor $ fun msg => IO.println msg;
         throw (IO.userError "failed to parse file")