problema con il comando "time": builtin o /usr/bin/time?

[Alberto Maurizi <".deb"@augh.net>]

	Ho un problema col comando time:

# which time
/usr/bin/time

# man time
SYNOPSIS
       time   [ -apqvV ] [ -f FORMAT ] [ -o FILE ]
              [ --append ] [ --verbose ] [ --quiet ] [ --portability ]
              [ --format=FORMAT ] [ --output=FILE ] [ --version ]
              [ --help ] COMMAND [ ARGS ]

# time -o qq ls
bash: -o: command not found

real    0m0.001s
user    0m0.000s
sys     0m0.001s

	mentre se eseguo
# /usr/bin/time -o qq ls

	ottengo il risultato descritto dalla man page).

	L'ho segnalato come bug (inconsistenza tra man e comando) ma mi
	hanno risposto che se eseguo "time" sto eseguendo un builtin
	della shell.

	Pero` "man builtins" mi dice che esiste il comando "times" e non
	time. E comunque "which time" mi dice che sto eseguendo
	/usr/bin/time, vero?

	Dove sto sbagliando?
	a.

-- 
Ci sono due specie di problemi: quelli che non si risolvono mai e quelli
che si risolvono da soli.
                -- Manuel Scorza, scrittore peruviano