# HG changeset patch # User wenzelm # Date 1300030202 -3600 # Node ID 380f7f5ff126e3ffa68f39b742150eba90fa0178 # Parent 8e32c3992cb3e51a564f8f459704d84fa9fc83ca proper File.shell_path; diff -r 8e32c3992cb3 -r 380f7f5ff126 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 13 16:14:14 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 13 16:30:02 2011 +0100 @@ -42,9 +42,9 @@ val _ = File.write code_file code' val _ = File.write narrowing_engine_file narrowing_engine val _ = File.write main_file main - val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc")) + val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc")) val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^ - (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^ + (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^ " -o " ^ executable ^ " && " ^ executable in bash_output cmd