# HG changeset patch
# User wenzelm
# Date 1440009683 -7200
# Node ID a0da65429a76d54d90782133aca176e16b9946a3
# Parent  c362c2d0f7251a0e02ce703cd598181a50b6c8d5
proper check for Windows executables;

diff -r c362c2d0f725 -r a0da65429a76 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Aug 19 19:54:02 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Aug 19 20:41:23 2015 +0200
@@ -167,7 +167,11 @@
         SOME var =>
         let
           val pref = getenv var ^ "/"
-          val paths = map (Path.explode o prefix pref) (snd exec)
+          val paths =
+            map (Path.explode o prefix pref)
+              (if ML_System.platform_is_windows then
+                map (suffix ".exe") (snd exec) @ snd exec
+               else snd exec);
         in
           (case find_first File.exists paths of
             SOME path => path