Ops. Remove bogus time calls.

diff --git a/make.sh b/make.sh
index 64a565b..8626c85 100755 (executable)
--- a/make.sh
+++ b/make.sh
@@ -113,9 +113,9 @@ sh make-config.sh || exit 1
 # Or, if you can set up the files somewhere shared (with NFS, AFS, or
 # whatever) between the host machine and the target machine, the basic
 # procedure above should still work, but you can skip the "copy" steps.
-time sh make-host-1.sh   || exit 1
-time sh make-target-1.sh || exit 1
-time sh make-host-2.sh   || exit 1
-time sh make-target-2.sh || exit 1
-time sh make-target-contrib.sh || exit 1
+sh make-host-1.sh   || exit 1
+sh make-target-1.sh || exit 1
+sh make-host-2.sh   || exit 1
+sh make-target-2.sh || exit 1
+sh make-target-contrib.sh || exit 1
 date