diff options
Diffstat (limited to 'envsetup.sh')
-rw-r--r-- | envsetup.sh | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/envsetup.sh b/envsetup.sh index a0dbf3d..4d9c58f 100644 --- a/envsetup.sh +++ b/envsetup.sh @@ -2092,7 +2092,7 @@ function mka() { make -j `sysctl hw.ncpu|cut -d" " -f2` "$@" ;; *) - schedtool -B -n 1 -e ionice -n 1 make -j$(cat /proc/cpuinfo | grep "^processor" | wc -l) "$@" + mk_timer schedtool -B -n 1 -e ionice -n 1 make -j$(cat /proc/cpuinfo | grep "^processor" | wc -l) "$@" ;; esac } @@ -2298,10 +2298,10 @@ function get_make_command() echo command make } -function make() +function mk_timer() { local start_time=$(date +"%s") - $(get_make_command) "$@" + $@ local ret=$? local end_time=$(date +"%s") local tdiff=$(($end_time-$start_time)) @@ -2336,6 +2336,11 @@ function make() return $ret } +function make() +{ + mk_timer $(get_make_command) "$@" +} + if [ "x$SHELL" != "x/bin/bash" ]; then case `ps -o command -p $$` in *bash*) |