aboutsummaryrefslogtreecommitdiff
path: root/ci/test_wholefile.v
AgeCommit message (Expand)Author
2020-05-04docs: Add a comment in ci/test_wholefile.vErik Martin-Dorel
2020-05-04test: Remove "Proof." workaroundErik Martin-Dorel
2020-05-04fix: Tweak comments and workaround ProofGeneral/PG#485Erik Martin-Dorel
2020-05-04test: Add tests and some fixCyril Anaclet