# HG changeset patch
# User wenzelm
# Date 1737108971 -3600
# Node ID 5900b58d6bd488102ffa66c315cba9c2c7de8bc9
# Parent  c84c0c0e6907ee41ce64aeba96e129cf5e0dabf9
clarified signature, following Isabelle/Scala;

diff -r c84c0c0e6907 -r 5900b58d6bd4 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Jan 17 11:05:36 2025 +0100
+++ b/src/Pure/General/path.ML	Fri Jan 17 11:16:11 2025 +0100
@@ -33,7 +33,6 @@
   val ext: string -> T -> T
   val platform_exe: T -> T
   val split_ext: T -> T * string
-  val exe: T -> T
   val expand: T -> T
   val file_name: T -> string
   eqtype binding
@@ -213,8 +212,6 @@
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
-val exe = ML_System.platform_is_windows ? ext "exe";
-
 
 (* expand variables *)
 
diff -r c84c0c0e6907 -r 5900b58d6bd4 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:05:36 2025 +0100
+++ b/src/Pure/Tools/generated_files.ML	Fri Jan 17 11:16:11 2025 +0100
@@ -343,7 +343,8 @@
         export |> List.app (fn (bindings, executable) =>
           bindings |> List.app (fn binding0 =>
             let
-              val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
+              val binding = binding0
+                |> Path.map_binding (executable = SOME true ? Path.platform_exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
                 (case try Bytes.read (dir + path) of