X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fscripts%2Finsert.awk;h=e38f341edb0a3122f09b2f5ad48077d768e138a4;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=267e893e2b967aa1a301179753af6ba8d0da2ac1;hpb=9d8e81db720417f58591ea42f72c6750b886a83d;p=helm.git diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk index 267e893e2..e38f341ed 100644 --- a/helm/matita/scripts/insert.awk +++ b/helm/matita/scripts/insert.awk @@ -1,18 +1,17 @@ - - -/^[^#]/ { - result=tolower($1); - if( $2 ~ "\.opt$" ) + { + result=tolower($3); + if( $1 ~ "\.opt$" ) compilation="opt" else compilation="byte" - test=$3 + test=$2 time="0:" $4 + timeuser="0:0:" $5 mark=$7 - if ( $8 ~ "^GC=off$") - options="'no-gc'" - else - options="''" + if ( $8 ~ "^gc-off$") + options="'gc-off'"; + if ( $8 ~ "^gc-on$") + options="'gc-on'" - printf "INSERT bench (result, compilation, test, time, mark, options) VALUES ('%s', '%s', '%s', '%s', '%s', %s);\n", result, compilation, test, time, mark, options; + printf "INSERT bench (result, compilation, test, time, timeuser, mark, options) VALUES ('%s', '%s', '%s', '%s', '%s', '%s', %s);\n", result, compilation, test, time, timeuser, mark, options; }