Commit afdeb066 authored by Heiko Becker's avatar Heiko Becker

Next script bugfix

parent a1f9305b
......@@ -84,7 +84,8 @@ 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}%%M2}
RESULT=${RESULT#M1}
RESULT=${RESULT%%M2}
echo -n $RESULT >>$1
cd ../../
......
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