2023-06-24 2023年6月24日 奥深きtimeコマンド 最近のtimeコマンド(というか、GNU timeコマンド)は単に実行時間がとれるだけじゃなく、各種リソースの消費状況も取れるのね。 atmarkit.itmedia.co.jp 明示的に/usr/bin/timeと打たないとGNU timeコマンドが使われない(インストールされていないこともある)のか。