merged
authorwenzelm
Mon Mar 21 17:14:52 2011 +0100 (2011-03-21)
changeset 42041f90040058a24
parent 42040 869df9b88deb
parent 42039 cef738d55348
child 42042 264f8d0e899f
child 42058 1eda69f0b9a8
merged
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 21 16:24:52 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 21 17:14:52 2011 +0100
     1.3 @@ -144,10 +144,9 @@
     1.4          val _ = File.write narrowing_engine_file narrowing_engine
     1.5          val _ = File.write main_file main
     1.6          val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
     1.7 -        val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
     1.8 +        val cmd = "( exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
     1.9            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.10 -          " -o " ^ executable ^ " && " ^ executable
    1.11 -          (* FIXME: should use bash command exec but does not work with && *) 
    1.12 +          " -o " ^ executable ^ "; ) && " ^ executable
    1.13        in
    1.14          bash_output cmd
    1.15        end