diff options
| author | coqbot-app[bot] | 2021-01-12 08:40:14 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-12 08:40:14 +0000 |
| commit | 702c96a5c191a22b5153f69e5104d76ae35190fc (patch) | |
| tree | 8b9de51ec0317b812c3bc873b72dd54310e03022 /dev/ci | |
| parent | 76de13a9ce03f542bca74dabee28bf27d9d8ac4f (diff) | |
| parent | 3c427cd52ad7e41b4a8cbb7e227b8f79730863b1 (diff) | |
Merge PR #13736: Do not declare a global universe object when this set is empty.
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions