blob: c594f8360363f70750c994e5cb537315b186d8f0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
#!/bin/bash
# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git
( cd fiat-crypto && make -j ${NJOBS} )
# ( cd corn && make -j ${NJOBS} )
|
