diff options
Diffstat (limited to 'tools/ci/ci-sf.sh')
| -rwxr-xr-x | tools/ci/ci-sf.sh | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/tools/ci/ci-sf.sh b/tools/ci/ci-sf.sh deleted file mode 100755 index 5e41211f1a..0000000000 --- a/tools/ci/ci-sf.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/bash - -ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh - -wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz -tar xvfz sf.tgz - -( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) - - |
