nigth-bench snapshot

[helm.git] / helm / matita / scripts / insert.awk

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
index 267e893e2b967aa1a301179753af6ba8d0da2ac1..e38f341edb0a3122f09b2f5ad48077d768e138a4 100644 (file)
--- 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;
        }