max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/path): user normalizePathSeparators at moduleNameOfFileName

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-28 10:09:51 -07:00
parent 17e5f0b719
commit 1d0d65893b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/path.lean
View file

@ -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