proper File.shell_path;
authorwenzelm
Sun Mar 13 16:30:02 2011 +0100 (2011-03-13)
changeset 41946380f7f5ff126
parent 41945 8e32c3992cb3
child 41947 0b8a13b145e9
proper File.shell_path;
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 16:14:14 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 16:30:02 2011 +0100
     1.3 @@ -42,9 +42,9 @@
     1.4          val _ = File.write code_file code'
     1.5          val _ = File.write narrowing_engine_file narrowing_engine
     1.6          val _ = File.write main_file main
     1.7 -        val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
     1.8 +        val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
     1.9          val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^
    1.10 -          (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^
    1.11 +          (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.12            " -o " ^ executable ^ " && " ^ executable
    1.13        in
    1.14          bash_output cmd