0.8.1.11:

[sbcl.git] / make.sh

diff --git a/make.sh b/make.sh
index 8626c85..64a565b 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.
-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
+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
 date