aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-10-30 14:16:13 +0100
committerPierre-Marie Pédrot2019-10-30 14:16:13 +0100
commit7634426a7a6de08ff0ea172a0770b9a159b25934 (patch)
treef65d556ad609d160b47379671262c64f10f893bc /dev/ci
parenta7371d946d44113a38d9cf217df36c23ce5e48ee (diff)
parentb27f54b04f50d3fad0eedd9c46366fd2bb612987 (diff)
Merge PR #10949: [declare] Provide helper for private constant inlining.
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions