Closed kelloggm closed 3 months ago
Actually, this PR should not be merged now (because we already have a fix for this, in #223).
However, that PR hasn't been merged because of other issues in the CI configuration (in specimin-evaluation), which need to have their fixes merged. Because this is an emergency, I'm going to override requirements on my fixes to the scripts in that repo so that I can merge #223 ASAP.
I can reproduce the failure locally and I'm now looking into it. I assume this is related to @tahiat's changes to the target repositories (to correct earlier mistakes in the version of the code we were targeting), but it should have been merged at the same time that those changes were made.