--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Mar 21 14:46:59 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Mar 21 16:38:28 2011 +0100
@@ -144,10 +144,9 @@
val _ = File.write narrowing_engine_file narrowing_engine
val _ = File.write main_file main
val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
- val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
+ val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
- " -o " ^ executable ^ " && " ^ executable
- (* FIXME: should use bash command exec but does not work with && *)
+ " -o " ^ executable ^ "; ) && " ^ executable
in
bash_output cmd
end