fix(lean/bin/leanpkg.bat): handle spaces in paths

Fixes leanprover#1973. I've tested it locally and this appears to be enough to solve the problem.
solson · Oct 7, 2018 · 374e711 · 374e711
1 parent b13ac12
commit 374e711
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/bin/leanpkg.bat b/bin/leanpkg.bat
@@ -2,8 +2,8 @@
 
 SET LEANDIR=%~dp0%../
 SET LIBDIR=%LEANDIR%\lib\lean
-IF NOT EXIST %LIBDIR% SET LIBDIR=%LEANDIR%
+IF NOT EXIST "%LIBDIR%" SET LIBDIR=%LEANDIR%
 SET LEAN_PATH=%LIBDIR%\library;%LIBDIR%\leanpkg
 SET PATH=%LEANDIR%\bin;%PATH%
 
-lean --run %LIBDIR%\leanpkg\leanpkg\main.lean %*
+lean --run "%LIBDIR%\leanpkg\leanpkg\main.lean" %*