diff options
| author | Hugo Herbelin | 2020-03-30 22:23:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-30 22:23:35 +0200 |
| commit | 8c85a8651605dd82ce2223a28ca38f31359a88bd (patch) | |
| tree | 4bda2eeb1d0c772e1b0d87fccde837d16f5ee4f1 /dev/tools/pre-commit | |
| parent | a78f7270b3416c3bffeac6d55a955811444416b3 (diff) | |
| parent | ea0bfc872a1363b47bf91e65fba0ecb770b39981 (diff) | |
Merge PR #11725: Cleanup stdlib reals.
Ack-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions