diff options
| author | Maxime Dénès | 2019-03-27 22:51:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-27 22:51:14 +0100 |
| commit | a796822e5f57f74ff36e538fd2169f70a8c6c145 (patch) | |
| tree | 56aaff0bd65a945471b27f5fab088aecf4d2459a /lib/system.ml | |
| parent | 738521ca3acb0f5b87cb1d23360350ed69f18cd1 (diff) | |
| parent | 2fc568a2661907eb6139ec7224fafb8f433aae2b (diff) | |
Merge PR #9827: Move code ownership of reals library to new maintainer team.
Reviewed-by: maximedenes
Diffstat (limited to 'lib/system.ml')
0 files changed, 0 insertions, 0 deletions