On Wed, Oct 14, 2015 at 5:58 PM, Bo Berglund <[email protected]> wrote: > On Mon, 12 Oct 2015 23:13:53 +0300, Juha Manninen > <[email protected]> wrote: > > $ time make clean bigide > > I have never seen such a command before, does it print the time the > command following time takes to complete??? > man time does not mention such a functionality... >
time is a builtin command (integrated in bash) thus to obtain help use 'help time'. Best regards, -Flávio -- _______________________________________________ Lazarus mailing list [email protected] http://lists.lazarus.freepascal.org/mailman/listinfo/lazarus
