From 1d0d65893b5bddef4e31e3a33c302bae52c7ac4c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jul 2019 10:09:51 -0700
Subject: [PATCH] fix(library/init/lean/path): user `normalizePathSeparators`
 at `moduleNameOfFileName`

---
 library/init/lean/path.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean
index bb4bc2ec9e..64ae8afc67 100644
--- a/library/init/lean/path.lean
+++ b/library/init/lean/path.lean
@@ -106,7 +106,7 @@ do fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
 def moduleNameOfFileName (fname : String) : IO Name :=
 do
 path  ← findAtSearchPath fname;
-fname ← IO.realPath fname;
+fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
 let fnameSuffix := fname.drop path.length;
 let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
 if path ++ pathSep ++ fnameSuffix != fname then