diff options
| author | Emilio Jesus Gallego Arias | 2019-04-01 21:32:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-01 21:32:38 +0200 |
| commit | 943fdd3277909f5229d95eb2e486944b0258648c (patch) | |
| tree | a8474b6f0f99759f7c00d506e7eac95c6be9a3a9 /dev/ci/docker | |
| parent | bb8c2bd25f4519fb0e3afccc956cee2c6d250491 (diff) | |
| parent | 73c924d3d4bcc22a179cb974603f9072599ebb77 (diff) | |
Merge PR #9874: [interp] [numeral] Improve numeral notations to support Ind and to not use the VM
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions