aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
authorPierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-07 14:17:21 +0100
committerPierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-07 14:17:21 +0100
commit84386f3353034b7b579ad1c28b0b2a4bf5c65043 (patch)
tree29bf00a8059af09f5e47bd71a68194fde988ef04 /riscV
parent3bb0c75456a0dcab079e7614c3bbd3ba971e4519 (diff)
downloadcompcert-84386f3353034b7b579ad1c28b0b2a4bf5c65043.tar.gz
compcert-84386f3353034b7b579ad1c28b0b2a4bf5c65043.zip
Fix check-proof target of the Makefile after merge of Coq #6277.
We simply fully qualify the modules. This is backward compatible.
Diffstat (limited to 'riscV')
0 files changed, 0 insertions, 0 deletions