summaryrefslogtreecommitdiff
path: root/Build
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2013-01-16 19:21:21 +0000
committerKarl Berry <karl@freefriends.org>2013-01-16 19:21:21 +0000
commit9c13d74d1fefc805938a4b1f94e14e6accd4163d (patch)
treeb58fafb6eda5e514a3699d540f85fa37b3074a08 /Build
parentc768f3052f5656eda2aab35eb9b339994abbea31 (diff)
allow override of the time program.
git-svn-id: svn://tug.org/texlive/trunk@28852 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Build')
-rwxr-xr-xBuild/source/Build9
1 files changed, 6 insertions, 3 deletions
diff --git a/Build/source/Build b/Build/source/Build
index 3fb7b1a567c..f244819be0a 100755
--- a/Build/source/Build
+++ b/Build/source/Build
@@ -24,7 +24,7 @@ if test -z "$TL_INSTALL_DEST"; then
TL_INSTALL_DEST=$H/inst
fi
-# allow override of make program.
+# allow override of the make program.
: ${TL_MAKE=make}
# make flags
@@ -38,6 +38,9 @@ export MAKE
: ${GNUMAKE=${TL_MAKE}}
export GNUMAKE
+# allow override of the time program, e.g., to /bin/true if you lack it.
+: ${TL_BUILD_TIME_PROG=time}
+
if test "x$1" = x--no-clean; then
shift
else
@@ -100,7 +103,7 @@ cd $TL_WORKDIR || exit 1
#
set -vx # show the configure and make commands in the log.
- eval $TL_BUILD_ENV time $TL_CONFIGURE \
+ eval $TL_BUILD_ENV $TL_BUILD_TIME_PROG $TL_CONFIGURE \
--prefix=$TL_INSTALL_DEST \
--datadir=$TL_INSTALL_DEST \
$TL_CONF_BANNER \
@@ -110,7 +113,7 @@ cd $TL_WORKDIR || exit 1
$TL_CONF_XDVI_TOOLKIT \
$TL_CONFIGURE_ARGS \
"$@" \
- && eval $TL_BUILD_ENV time $TL_MAKE $TL_MAKE_FLAGS $TL_TARGET
+ && eval $TL_BUILD_ENV $TL_BUILD_TIME_PROG $TL_MAKE $TL_MAKE_FLAGS $TL_TARGET
# Too arcane to try to propagate the exit status through a pipeline.
# Just use a temp file.