Remove developer script not needed in git repository

This commit is contained in:
Xavier Claessens 2018-06-04 22:25:10 -04:00
parent b04cf01934
commit 27ec1469ab

View File

@ -1,6 +0,0 @@
#!/bin/sh
DIR=`dirname $0`;
(cd $DIR; make performance)
ID=`git rev-list --max-count=1 HEAD`
echo "Testing revision ${ID}"
$DIR/performance | tee "perf-${ID}.log"