Replace "tee" by a python scripts that should work on any system.

diff --git a/tools/make-batch b/tools/make-batch
index 5358751129a69107f834380bdd5f21190c10518d..b1cf92612e928422d49704a91cbeb7b91383d71d 100644 (file)
--- a/tools/make-batch
+++ b/tools/make-batch
@@ -47,7 +47,7 @@ batch_attach() {
 ###############################################################################
 batch_run() {  
        gettoolchain
-       $0 build | tee $BATCHLOG
+       $0 build | $BASEDIR/tools/tee $BATCHLOG
        sleep 5
        if [ -e $FAILED ]; then
                SUBJECT="Failed :("

diff --git a/tools/tee b/tools/tee
new file mode 100755 (executable)
index 0000000..65097ad
--- /dev/null
+++ b/tools/tee
@@ -0,0 +1,27 @@
+#! /usr/bin/python
+
+import os
+import sys
+from select import select
+
+targets = [sys.stdout]
+for filename in sys.argv[1:]:
+       f = open(filename, "w")
+       targets.append(f)
+
+targetfds = []
+for f in targets:
+       targetfds.append(f.fileno())
+
+src = sys.stdin.fileno()
+while 1:
+    (r, w, x) = select([src],[],[])
+    str = os.read(src,1)
+    if str == '':
+        break
+
+    for fd in targetfds:
+        os.write(fd, str)
+
+for f in targets:
+       f.close()