Commit 5b7e6db5 authored by Heiko Becker's avatar Heiko Becker

Fix script typo

parent 99b646c4
......@@ -84,7 +84,7 @@ do
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" >>$2
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#M1}
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment