--- a/src/Pure/General/file.ML Sun Sep 20 20:00:14 2020 +0200
+++ b/src/Pure/General/file.ML Sun Sep 20 20:47:59 2020 +0200
@@ -10,6 +10,7 @@
val platform_path: Path.T -> string
val bash_path: Path.T -> string
val bash_paths: Path.T list -> string
+ val bash_platform_path: Path.T -> string
val full_path: Path.T -> Path.T -> Path.T
val tmp_path: Path.T -> Path.T
val exists: Path.T -> bool
@@ -50,6 +51,8 @@
val bash_path = Bash_Syntax.string o standard_path;
val bash_paths = Bash_Syntax.strings o map standard_path;
+val bash_platform_path = Bash_Syntax.string o platform_path;
+
(* full_path *)