Мне нужно выполнить команду и получить время ее выполнения.Я использую 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