Skip to content

add back the ability to skip reference file checks on some Coq versions

Ralf Jung requested to merge ralf/noref into master

Alternative to !1009 (closed): just don't test reference files on 8.19 for now.

Having printing output reference files for multiple Coq versions would be possible, but that's a huge hassle. Iris contributors that change tests need to compile with multiple Coq versions to update both .ref files.

We had that infrastructure, but I agree it's not great, so I removed it.

Merge request reports