# HG changeset patch
# User wenzelm
# Date 1554384378 -7200
# Node ID 997f256c98e323691a47d8c8251aa5fc0176d43e
# Parent  a670d20c600dcd3e9ed43a6c7114522769fb0189
proper .exe path for export;

diff -r a670d20c600d -r 997f256c98e3 src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML	Thu Apr 04 14:45:34 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML	Thu Apr 04 15:26:18 2019 +0200
@@ -267,9 +267,10 @@
             ML_Lex.read_source source @ ML_Lex.read ")");
       val _ =
         export |> List.app (fn (bindings, executable) =>
-          bindings |> List.app (fn binding =>
+          bindings |> List.app (fn binding0 =>
             let
-              val (path, pos) = Path.dest_binding binding |>> executable = SOME true ? Path.exe;
+              val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
+              val (path, pos) = Path.dest_binding binding;
               val content =
                 (case try File.read (Path.append dir path) of
                   SOME context => context