clarified signature;
authorwenzelm
Wed, 15 Jul 2020 12:30:25 +0200
changeset 72266 e48a5b6b7554
parent 72265 25d5ef16401a
child 72267 aa6a36c730c9
clarified signature;
src/Pure/Admin/build_cygwin.scala
src/Pure/General/file.scala
--- a/src/Pure/Admin/build_cygwin.scala	Wed Jul 15 12:04:48 2020 +0200
+++ b/src/Pure/Admin/build_cygwin.scala	Wed Jul 15 12:30:25 2020 +0200
@@ -42,7 +42,7 @@
           progress.bash(
             File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" +
               " --local-package-dir 'C:\\temp'" +
-              " --root " + Bash.string(File.platform_path(cygwin)) +
+              " --root " + File.bash_platform_path(cygwin) +
               " --packages " + quote((packages ::: more_packages).mkString(",")) +
               " --no-shortcuts --no-startmenu --no-desktop --quiet-mode",
             echo = true)
--- a/src/Pure/General/file.scala	Wed Jul 15 12:04:48 2020 +0200
+++ b/src/Pure/General/file.scala	Wed Jul 15 12:30:25 2020 +0200
@@ -124,6 +124,8 @@
   def bash_path(path: Path): String = Bash.string(standard_path(path))
   def bash_path(file: JFile): String = Bash.string(standard_path(file))
 
+  def bash_platform_path(path: Path): String = Bash.string(platform_path(path))
+
 
   /* directory entries */