diff options
| author | Emilio Jesus Gallego Arias | 2019-02-18 19:43:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 19:43:43 +0100 |
| commit | a4a59ec5cf426bb1ee36dc1ac49cb20bd17d5f43 (patch) | |
| tree | 466c6643c909f0df08dbc7ed8443e7283a2123e1 /gramlib | |
| parent | 69f219cdcddc10823d52ffa1ea9503254e48bce4 (diff) | |
| parent | 6d54c0fbbe8c905991dcb99112cce69792c9b142 (diff) | |
Merge PR #9589: Deprecate duplicated explicitation_eq
Reviewed-by: ejgallego
Reviewed-by: herbelin
Ack-by: jashug
Diffstat (limited to 'gramlib')
0 files changed, 0 insertions, 0 deletions