diff options
| author | Emilio Jesus Gallego Arias | 2020-02-23 15:42:51 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-23 15:42:51 -0500 |
| commit | b04f8948b167ef227372eeffe299462b6bde1f1b (patch) | |
| tree | a5fbba65180fdf8d9a1ae6a7a9a16f99159328c1 /dev/tools | |
| parent | c4259da61f63ff6c2b088398a6f7fae31a2ebeb2 (diff) | |
| parent | e715ae132c84960f766d64e7a17eea74924eadab (diff) | |
Merge PR #11660: Fix #11654: syntax of inductive declaration.
Reviewed-by: ejgallego
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions