diff options
| author | Gaëtan Gilbert | 2018-11-14 13:40:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:10:21 +0100 |
| commit | 1310a684c8dbcbf3c94022c8e9b6cec3bf092e3d (patch) | |
| tree | b59c1382c249ab7609ef43123df8f9f79d871345 /dev | |
| parent | 6133c0633f4a3545de4017325d0f213fbbb5c07d (diff) | |
Use universe names when printing to dot.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions