diff options
| author | Maxime Dénès | 2017-08-29 17:10:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-29 17:10:49 +0200 |
| commit | f67ebbba77998e6469ad0fc9dc80b306ab2e62ce (patch) | |
| tree | dd040de44efa3cc130a7c010bccaf8c996bdc73a /kernel | |
| parent | a980d38681f7ab9bfd8a180f2252ce573e3ff211 (diff) | |
| parent | 8a9dede5b78ba7a34e478d19e62e2648f207c3a8 (diff) | |
Merge PR #988: Fix obsolete description of real numerals.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions