# HG changeset patch # User wenzelm # Date 1220551548 -7200 # Node ID b82ddffe7429f08b65796cca91c03f1fd8e76ad7 # Parent 6c7f005cfef8f0cf535dbcab3c4a1b82136bb989 init: disallow "" as out stream; diff -r 6c7f005cfef8 -r b82ddffe7429 src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Thu Sep 04 19:47:13 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.ML Thu Sep 04 20:05:48 2008 +0200 @@ -100,7 +100,7 @@ fun setup_channels out = let val out_stream = - if out = "" orelse out = "-" then TextIO.stdOut + if out = "-" then TextIO.stdOut else let val path = File.platform_path (Path.explode out);