diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-08 20:28:36 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-08 20:28:36 +0000 |
| commit | ce80e570ff7c3db0c469bca19f7bcf088b4b6304 (patch) | |
| tree | 3d2dc79c24942289faeaedfbc42247eed86f0689 /contrib | |
| parent | 8b84abb2a69ef595b4ccae8bde56414dd3fa295c (diff) | |
Moving cluster-qf_lra-benchmark to scripts project
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/cluster-qf_lra-benchmark | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/contrib/cluster-qf_lra-benchmark b/contrib/cluster-qf_lra-benchmark deleted file mode 100755 index 1311d869c..000000000 --- a/contrib/cluster-qf_lra-benchmark +++ /dev/null @@ -1,18 +0,0 @@ - -TO_EMAIL="taking@cs.nyu.edu" -CC_EMAIL="" -function RunClusterRegressions() { - local job_name="cvc4-$1" - local cvc4_binary="$2" - local config_line="$3" - mysql -u smt_cluster --password=`cat ~/.mysql_password` smt_cluster <<EOF - insert into Jobs values - (DEFAULT, "$job_name", "custom job", "19", "300", "2000", "26", "$TO_EMAIL $CC_EMAIL", "2", "$cvc4_binary", "1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29", DEFAULT); -EOF -} - - -JOB_TIME=`date +%s` -NAME="cluster-qf_lra-benchmark-$JOB_TIME" -RunClusterRegressions "$NAME" $1 "" - |