diff options
| author | coqbot-app[bot] | 2021-01-22 09:36:39 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-22 09:36:39 +0000 |
| commit | 7d5618684ef17fbb34246f041b3426d42825b85a (patch) | |
| tree | 24deae282c6a10518d3c3735919a896c499d60ec /library | |
| parent | 2f79b58cdbdeb3ff3446168ede042e063a6f6c99 (diff) | |
| parent | 56578a246e6b13d539fd6b0f54f7e06c641fd847 (diff) | |
Merge PR #13775: Improve wording for #13384 (Warn on hints without an explicit locality)
Reviewed-by: Zimmi48
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions