Hi,
I noticed that on my jedit build Cache_IO.run is not giving intended
result. I tested it with the attached theory file. From jedit output, I
get this result:
val it = {output = [], return_code = 1, redirected_output = []}:
Cache_IO.result
However, when the same file is run in
On Sun, 24 Jul 2011, Sree Harsha Totakura wrote:
Hi,
I noticed that on my jedit build Cache_IO.run is not giving intended
result. I tested it with the attached theory file. From jedit output, I
get this result:
val it = {output = [], return_code = 1, redirected_output = []}:
