diff options
| author | Pierre-Marie Pédrot | 2019-05-14 23:20:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 23:20:18 +0200 |
| commit | 75262c3f8af195a83673ff06a53d0fd0bd23b57e (patch) | |
| tree | d658e13c19c37e77eb220eb0bf0872c27bf5b653 /dev/ci | |
| parent | c0d4e5b42da59177f2829e4103fcc8c088548a18 (diff) | |
| parent | a17626eb716b8a7b0ae5c1387f485223ba1c2de5 (diff) | |
Merge PR #10136: [ltac2] Add primitive integers
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions