another step roward the removal of do_tests.sh

diff --git a/helm/software/matita/scripts/README b/helm/software/matita/scripts/README
index d48449056c4262fa978c8777a15024a2e2fbca5d..831fbbd9035868f603ad294127b4bde8d157ac64 100644 (file)
--- a/helm/software/matita/scripts/README
+++ b/helm/software/matita/scripts/README
@@ -12,9 +12,6 @@ do_tests.sh
   script used by ../Makefile to run matitac[.opt] on some tests. supports some
   options and prints out some informations neded my insert
 
-insert.awk  
-  creates the SQL INSERT statements for the output of profile_cvs.sh
-
 profile_svn.sh
   SVN co, compilation, run
 

diff --git a/helm/software/matita/scripts/insert.awk b/helm/software/matita/scripts/insert.awk
deleted file mode 100644 (file)
index d62a6a3..0000000
--- a/helm/software/matita/scripts/insert.awk
+++ /dev/null
@@ -1,17 +0,0 @@
- {
-       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;
-       }