diff --git a/envsetup.sh b/envsetup.sh index a0f633f25..3b8507f65 100644 --- a/envsetup.sh +++ b/envsetup.sh @@ -1473,37 +1473,6 @@ 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*)