diff options
| author | Emilio Jesus Gallego Arias | 2019-01-27 17:25:46 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-27 17:25:46 +0100 |
| commit | c2031832ddcf1f631ef86cdb4c0dafeb9b742c79 (patch) | |
| tree | a393f15b9d59eb8ae19bba13058ed54dfd1d4770 /dev | |
| parent | 4b006833d6f866a33024e674d300f74592d24622 (diff) | |
| parent | 25014277624387ecba1befb60f1c54d68eadab01 (diff) | |
Merge PR #9214: Notations: Removing useless parentheses on abbreviations shortening a strict prefix of an application
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions