aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-corn.sh
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-01-22 17:35:02 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-20 14:44:58 +0100
commit041ee4822cb247e60df51fa147175f8b16711df1 (patch)
tree49e61993afab55d44d9642f5dcaebf36fa6cd94b /dev/ci/ci-corn.sh
parentaec63ba9c8f6840d98ba731640a786138d836343 (diff)
proofview: goals come with a state
Diffstat (limited to 'dev/ci/ci-corn.sh')
0 files changed, 0 insertions, 0 deletions