diff --git a/envsetup.sh b/envsetup.sh index 3b8507f654..a0f633f25d 100644 --- a/envsetup.sh +++ b/envsetup.sh @@ -1473,6 +1473,37 @@ function pez { return $retval } +MAKE_UTIL=(`which make`) +function make() +{ + local start_time=$(date +"%s") + $MAKE_UTIL $@ + local ret=$? + local end_time=$(date +"%s") + local tdiff=$(($end_time-$start_time)) + local hours=$(($tdiff / 3600 )) + local mins=$((($tdiff % 3600) / 60)) + local secs=$(($tdiff % 60)) + echo + if [ $ret -eq 0 ] ; then + echo -n -e "\e[0;32m#### make completed successfully " + else + echo -n -e "\e[0;31m#### make failed to build some targets " + fi + if [ $hours -gt 0 ] ; then + printf "(%02g:%02g:%02g (hh:mm:ss))" $hours $mins $secs + elif [ $mins -gt 0 ] ; then + printf "(%02g:%02g (mm:ss))" $mins $secs + elif [ $secs -gt 0 ] ; then + printf "(%s seconds)" $secs + fi + echo -e " ####\e[00m" + echo + return $ret +} + + + if [ "x$SHELL" != "x/bin/bash" ]; then case `ps -o command -p $$` in *bash*)