Allow immediate output of spawned processes for all platforms.

[features.git] / src / support / os.h

diff --git a/src/support/os.h b/src/support/os.h
index 1644ef4bf001eac42a13bae957aa28999736e720..cbfd7c5d03119ccfadfb0711e7326b1665532792 100644 (file)
--- a/src/support/os.h
+++ b/src/support/os.h
@@ -39,12 +39,6 @@ void init(int argc, char * argv[]);
 /// Returns the name of the NULL device (/dev/null, null).
 std::string const & nulldev();
 
-/// Returns the name of the stdout device (/dev/stdout, /dev/tty, conout$).
-std::string const & stdoutdev();
-
-/// Returns the name of the stderr device (/dev/stderr, /dev/tty, conout$).
-std::string const & stderrdev();
-
 /// Tells whether \p channel is connected to a terminal or not. 
 bool is_terminal(io_channel channel);