projects
/
helm.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
194661b
)
override USER with bench
author
Enrico Tassi
<enrico.tassi@inria.fr>
Sat, 23 Sep 2006 15:44:45 +0000
(15:44 +0000)
committer
Enrico Tassi
<enrico.tassi@inria.fr>
Sat, 23 Sep 2006 15:44:45 +0000
(15:44 +0000)
matita/scripts/profile_svn.sh
patch
|
blob
|
history
diff --git
a/matita/scripts/profile_svn.sh
b/matita/scripts/profile_svn.sh
index 296ad125d62024aa8ac1f0ab88c75d60ee158084..b5ddfb0f622a553ee82f8f06af05d4884f989a10 100755
(executable)
--- a/
matita/scripts/profile_svn.sh
+++ b/
matita/scripts/profile_svn.sh
@@
-59,6
+59,7
@@
ln -s trunk/helm .
#compile
export HOME="`pwd`/../$TMPDIRNAME.HOME"
+export USER="bench"
compile $PWD/helm/software/
#run
@@
-66,7
+67,7
@@
run_tests $PWD/helm/software/matita > LOG 2>LOG.run_tests.err
#insert the db
cat LOG | grep "\(OK\|FAIL\)" | grep "\(gc-on\|gc-off\)" | \
- $PWD/helm/software/matita/scripts/functions.lua log2sql - > INSERT.sql
+
lua50
$PWD/helm/software/matita/scripts/functions.lua log2sql - > INSERT.sql
cat INSERT.sql | $MYSQL
#save the revision