test branch

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

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
new file mode 100644 (file)
index 0000000..d62a6a3
--- /dev/null
+++ b/helm/matita/scripts/insert.awk
@@ -0,0 +1,17 @@
+ {
+       result=tolower($3);
+       if( $1 ~ ".opt$" )
+               compilation="opt"
+       else
+               compilation="byte"
+       test=$2 
+       time=$4
+       timeuser=$5
+       mark=$7
+       if ( $8 ~ "^gc-off$") 
+               options="'gc-off'";
+       if ( $8 ~ "^gc-on$") 
+               options="'gc-on'"
+               
+       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;
+       }