diff -r b452242dce36 -r 7d0861af3cb0 src/Pure/General/path.ML
--- 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], "")