Merge pull request #8596 from Mikolaj/urlopen-timeout-CI-5th-attempt
commit4cdaa50afc99df758b9b754a6fb00f8723172c2f
authorMikolaj Konarski <mikolaj@well-typed.com>
Wed, 16 Nov 2022 10:30:02 +0000 (16 11:30 +0100)
committerGitHub <noreply@github.com>
Wed, 16 Nov 2022 10:30:02 +0000 (16 11:30 +0100)
tree53707f8787df9bbb6a30d95bfaa2fd20ac5a9dc1
parent40b631804e026077d3acce59381cb3b2b42066fd
parent369ebefea144474f25e4735b65e243eba6286ff5
Merge pull request #8596 from Mikolaj/urlopen-timeout-CI-5th-attempt

Hardwire a different CI cache path, to fix CI