aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorJason Gross2019-11-26 15:28:38 -0500
committerJason Gross2019-11-27 13:19:29 -0500
commit309c7ae0ea95d2ca4ade8a6ba88e92ab9b7c08f0 (patch)
tree827daa6962d63839560b434d017b1521661aa4a4 /dev/ci/ci-basic-overlay.sh
parent353b601323ffd7d5b4acc3c02de985b27cddc8e5 (diff)
[ci] Build slightly more in the fiat-crypto target
This adds a couple extra files, but not many.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions