我需要执行一个命令并获取它的执行时间。我正在使用 gtime 但输出与我想要的有点不同。
gtime 返回执行结果,然后返回执行时间。我需要将命令的输出(我需要它只是时间)存储在一个变量中,然后再使用它。有没有办法更改命令以仅获取执行时间?
所以如果我写下面的命令:
executiontime=$(gtime -f "%U" /Users/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2)
echo "$executiontime"
那么这是我得到的输出示例:
sat
(objectives
(misses_80 1)
)
9.94