diff options
| author | Théo Zimmermann | 2019-03-25 16:32:40 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-25 16:32:40 +0100 |
| commit | 2fc568a2661907eb6139ec7224fafb8f433aae2b (patch) | |
| tree | 9d55ada43329571013b5f49d5610d1cb78522509 /lib/system.ml | |
| parent | fd065eae52dde32bcb95955f6da9280fed780729 (diff) | |
Move code ownership of reals library to new maintainer team.
Diffstat (limited to 'lib/system.ml')
0 files changed, 0 insertions, 0 deletions