time command in bash is aliased or defined... but how?
I'm getting some strange behavior of the time command. It ignores command options. It must have been redefined, but I can't find an alias or function for it, so I don't know how it has been redefined. Here is what I am seeing:
Normal time command (no options): Code:
$ time sleep 0.1 Code:
$ time --format="%e" sleep 0.1 If I give the full path of the executable, it works fine: Code:
$ /usr/bin/time sleep 0.1 Diagnostics: I am running Debian 7.5 (Wheezy). I checked .bashrc and .profile in my home directory. I checked /etc/bash.bashrc, /etc/profile, and files in the /etc/profile.d directory. I checked env. I checked alias. I tried which and whereis. I checked $PATH. I tried unset -f time. Code:
$ uname -a Help! Also I am wondering how I can tell what other bash commands might have been redefined so that they do not work as described in the manual. |
there are two different time commands available. One is the shell's built-in and the second one is /usr/bin/time. Do not mix them!
|
Quote:
Okay, I've just read man bash-builtins and don't see a built-in function by that name... ... but I do see in man bash that time is a reserved word: Code:
RESERVED WORDS Code:
Users of the bash shell need to use an explicit path in order to run |
you are welcome
just use: type time which time |
Quote:
Code:
$ type time |
All times are GMT -5. The time now is 12:35 PM. |