--- a/src/Pure/General/path.ML Thu Oct 15 13:24:16 2020 +0200
+++ b/src/Pure/General/path.ML Thu Oct 15 13:47:55 2020 +0200
@@ -32,6 +32,7 @@
val dir: T -> T
val base: T -> T
val ext: string -> T -> T
+ val platform_exe: T -> T
val split_ext: T -> T * string
val exe: T -> T
val expand: T -> T
@@ -212,6 +213,8 @@
fun ext "" = I
| ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
+val platform_exe = ML_System.platform_is_windows ? ext "exe";
+
val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
(case chop_suffix (fn c => c <> ".") (raw_explode s) of
([], _) => (Path [Basic s], "")