# HG changeset patch # User wenzelm # Date 1594809025 -7200 # Node ID e48a5b6b755465b39ac2a2ca70d2b53da2ad0b87 # Parent 25d5ef16401a5d7d66664c5cdce3f8960686655a clarified signature; diff -r 25d5ef16401a -r e48a5b6b7554 src/Pure/Admin/build_cygwin.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) diff -r 25d5ef16401a -r e48a5b6b7554 src/Pure/General/file.scala --- 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 */