diff options
| author | Gaëtan Gilbert | 2017-06-13 21:43:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-06-20 12:23:19 +0200 |
| commit | a2bc4d3be684ad24ea7888df4dd0cf35d9733c64 (patch) | |
| tree | 054f4dac6eed0adbc86aa4a608d8d28493afdf22 /dev/ci/ci-basic-overlay.sh | |
| parent | d30ed5fe0694466f70eed51bc689cd0fa8c00da5 (diff) | |
Remove dead code [Universes.simplify_universe_context]
Dead since 23f4804b50307766219392229757e75da9aa41d9
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions