diff options
| author | Théo Zimmermann | 2019-04-03 10:01:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-04-03 10:01:02 +0200 |
| commit | ae3c0e70f1d3f8d8d7c338ffd18b179968e920aa (patch) | |
| tree | 210bc20148a9f341e06aff6a2a93ce8afeb5f2dc /lib/control.mli | |
| parent | 8f37727a0cb99eb7f250bd507635de6628de23ad (diff) | |
| parent | 5f3663cb57b2e12c498a92bd5d50454d95f6f257 (diff) | |
Merge PR #9896: Minor correction to numeral notations doc
Reviewed-by: Zimmi48
Diffstat (limited to 'lib/control.mli')
0 files changed, 0 insertions, 0 deletions