diff options
| author | Pierre-Marie Pédrot | 2020-01-28 13:00:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-28 13:00:44 +0100 |
| commit | 36c61df9435ce382084ddb097ffe0c7b2e220cbb (patch) | |
| tree | d0908b97193ffe5dee9c95a5be2f40e0d563d0d9 /dev | |
| parent | 2b4ebc5cd24f131567052d64889b2d24d5cc5ee8 (diff) | |
| parent | f011a88bd4be4797617741d6829d2530bc29ebdf (diff) | |
Merge PR #11419: schemes: use rigid universes
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions