etc/ci/remove_autogenerated.sh


1
2
3
4
5
6

#!/usr/bin/env bash

cd "$( dirname "${BASH_SOURCE[0]}" )"
cd ../..
sed s'|^src/Specific/montgomery.*||g' -i _CoqProject
sed s'|^src/Specific/solinas.*||g' -i _CoqProject