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 */