Started 5 days 6 hr ago
Took 17 min on research-jenkins-worker-08

Success Build #1077 (Feb 12, 2019 9:07:59 AM)

PR #637: Vastly simplify the set of ...
No changes.

GitHub pull request #637 of commit 4616433c1e0446cc6328af6a76c5133a65cf364c automatically merged.