--- ./Tools/xtermpipe/xtermpipe.cxx.orig 2012-08-24 12:25:01.293914000 +0200 +++ ./Tools/xtermpipe/xtermpipe.cxx 2012-08-24 12:35:23.714913382 +0200 @@ -40,6 +40,7 @@ return(1); } +int main() { int read_id, write_id;