diff options
| author | Pierre-Marie Pédrot | 2018-05-15 21:59:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-15 21:59:54 +0200 |
| commit | e95c5e6d92ba9ab776444ca1376d45c584acab50 (patch) | |
| tree | 2d1233b27a44c291448c1fb091a9683c23af05c4 /dev | |
| parent | 927b3826e645d428ebe3d8c6599c1f9e2bf79d46 (diff) | |
| parent | 96a357777e2e3c1273a61e0767bc04085d56835e (diff) | |
Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation function
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions