aboutsummaryrefslogtreecommitdiff
path: root/.github/workflows/metrics.yaml
diff options
context:
space:
mode:
authorbors[bot] <26634292+bors[bot]@users.noreply.github.com>2021-04-02 12:25:40 +0100
committerGitHub <[email protected]>2021-04-02 12:25:40 +0100
commit00ce7ae5248b41d5944abe6075407236cde1b075 (patch)
treea7d300232f331eb2d4e854e884c8d8c0d60404c6 /.github/workflows/metrics.yaml
parenta0b3eb7135361315ed953613a1a8c7a038b1562d (diff)
parent0e8c4503bf4754f4437d8bd45a110b9d0ec671e0 (diff)
Merge #8285
8285: Don't recheck obligations if we have learned nothing new r=matklad a=flodiebold This is just the most trivial check: If no inference variables have been updated, and there are no new obligations, we can just skip trying to solve them again. We could be smarter about it, but this already helps quite a bit, and I don't want to touch this too much before we replace the inference table by Chalk's. Fixes #8263 (well, improves it quite a bit). Co-authored-by: Florian Diebold <[email protected]>
Diffstat (limited to '.github/workflows/metrics.yaml')
0 files changed, 0 insertions, 0 deletions