X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fscripts%2Finsert.awk;h=d62a6a3ecdc2aef395833e1a6a04dc068c017288;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=267e893e2b967aa1a301179753af6ba8d0da2ac1;hpb=9d8e81db720417f58591ea42f72c6750b886a83d;p=helm.git

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
index 267e893e2..d62a6a3ec 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	
-	time="0:" $4
+	test=$2	
+	time=$4
+	timeuser=$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;
 	}