]> matita.cs.unibo.it Git - helm.git/commitdiff
go
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 21 Mar 2006 13:58:58 +0000 (13:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 21 Mar 2006 13:58:58 +0000 (13:58 +0000)
matita/scripts/public_html/bench.php
matita/scripts/public_html/common.php

index 0a3d4fde54ce10048dad33a06a11508c614068df..84f27d6e2a6efbac8c4d5855f137fbee11e7f4d1 100644 (file)
@@ -173,7 +173,17 @@ function links_of($name,$q,$limits){
 <tr><td></td></tr>
 <tr><td>SQL (only one query, ';' if present must terminate the query, no characters allowed after it):</td></tr>
 <tr><td>
-<textarea rows="10" cols="80" name="query"/>select SUM(time) from bench;</textarea>
+<textarea rows="10" cols="120" name="query"/>
+select 
+  b1.test as test, b1.timeuser as oldtime, b2.timeuser as newtime, b1.compilation as comp, b1.options as opts
+from 
+  bench as b1, bench as b2 
+where 
+  b1.test = b2.test and 
+  b1.options = b2.options and
+  b1.compilation = b2.compilation and 
+  b1.mark = '' and b2.mark= '' and
+  ABS(b1.timeuser - b2.timeuser) &gt; 100;</textarea>
 </td>
 </tr>
 <tr><td>
index 48121b5498ad748ff80ffff815bdd6fef0bfb483..0e7962abfae84b2aff4a64c1f9031dc2583e7258 100644 (file)
@@ -50,8 +50,9 @@ function printer($q){
 function query($q,$f) {
   $db = mysql_pconnect("localhost","helm");
   mysql_select_db("matita");
+  $q = preg_replace("/\n/"," ",$q);
   if (!preg_match("/^(select|describe)[^\n;]*;?$/i",$q)) {
-    echo "Query not allowed!";
+    die("Query not allowed!<pre>" . $q . "</pre>");
     return;
   }
   $rc = mysql_query($q,$db);