diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 10:58:52 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-10 10:58:52 +0200 |
| commit | b6d4575e39d32d276bed84ccb6b2b67a2e7bccb6 (patch) | |
| tree | bae13dd9fe715a0d9b095af44449b1c65c973829 /kernel/term_typing.mli | |
| parent | a2e283c8545f9e7f2951c42892945b027674a665 (diff) | |
| parent | c51567b3c651e72bf5ddf398b7428960cb7ff078 (diff) | |
Merge PR #1137: Include leading zeros in version info
Diffstat (limited to 'kernel/term_typing.mli')
0 files changed, 0 insertions, 0 deletions