# 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