aboutsummaryrefslogtreecommitdiff
path: root/dev/include_printers
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-11 18:19:11 +0000
committerGitHub2021-02-11 18:19:11 +0000
commit5b0bbc0ecd4effd77c7bd575f37d8996b519c65c (patch)
tree3f339bcd214133a088bc341456182ffc0a2425c3 /dev/include_printers
parentd7199fb0c9677d7a2a2e2b6d9fad61e13d22286a (diff)
parent4b08c87c99a72dd57bdd5b0be1bddd4085b4d495 (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/include_printers')
0 files changed, 0 insertions, 0 deletions