diff options
| author | Jason Gross | 2020-05-19 15:31:50 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-20 15:18:09 -0400 |
| commit | 8263c13919ca5a9ea59bc7cb930117215ddec3a9 (patch) | |
| tree | 3d0659f65bf6a8369a2566087409b8933f1a9934 /dev/ci | |
| parent | 19a231af66b275e83989e947b373cd44a889a319 (diff) | |
[merge-pr] Use a simpler method to get all pages
h/t SkySkimmer at
https://github.com/coq/coq/pull/12316#issuecomment-630952659
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions