diff options
| author | coqbot-app[bot] | 2021-02-11 18:19:11 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-11 18:19:11 +0000 |
| commit | 5b0bbc0ecd4effd77c7bd575f37d8996b519c65c (patch) | |
| tree | 3f339bcd214133a088bc341456182ffc0a2425c3 /dev | |
| parent | d7199fb0c9677d7a2a2e2b6d9fad61e13d22286a (diff) | |
| parent | 4b08c87c99a72dd57bdd5b0be1bddd4085b4d495 (diff) | |
Merge PR #13831: Properly document the local and global locality attributes.
Reviewed-by: gares
Reviewed-by: jfehrle
Ack-by: SkySkimmer
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions