diff options
| author | Gaëtan Gilbert | 2017-09-20 19:45:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-25 14:18:35 +0100 |
| commit | 280c922fc55b57c430cad721c83650a796a375fd (patch) | |
| tree | 5f0c9c20a75532ba134bbde6f428facefceb5125 /API/API.mli | |
| parent | c93d5094bff73498ec8fc02837e16cc5ce9103b6 (diff) | |
Allow local universe renaming in Print.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions