# HG changeset patch # User wenzelm # Date 1602762475 -7200 # Node ID 7d0861af3cb00b49b6e2a97bb4510d2f1f8e2855 # Parent b452242dce3603d23fdf5ddaa27c1e0c77d5affd proper support for Windows exe; diff -r b452242dce36 -r 7d0861af3cb0 src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Thu Oct 15 13:24:16 2020 +0200 +++ b/src/HOL/Tools/SMT/smt_systems.ML Thu Oct 15 13:47:55 2020 +0200 @@ -18,7 +18,9 @@ fun check_tool var () = (case getenv var of "" => NONE - | s => if File.is_file (Path.variable var) then SOME [s] else NONE); + | s => + if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe) + then SOME [s] else NONE); fun make_avail name () = getenv (name ^ "_SOLVER") <> "" 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], "")