]>
matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/scripts/insert.awk
{
result=tolower($3);
- if( $1 ~ "\.opt$" )
+ if( $1 ~ ".opt$" )
compilation="opt"
else
compilation="byte"
test=$2
- time="0:" $4
- timeuser="0:0:" $5
+ time=$4
+ timeuser=$5
mark=$7
if ( $8 ~ "^gc-off$")
options="'gc-off'";