aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-24 15:54:19 +0000
committerGitHub2020-11-24 15:54:19 +0000
commitb4cc5fa61236b6c6d716d2cf19947022658bd570 (patch)
tree61db04e10b743878039ae25d882e79df49b1eb63 /dev
parent90cb2b0daf54cbd72c5ac8e1ffe2007c8901ddba (diff)
parent60ed425ffc8bc30c11a3a8e542a9bfb0a0a06471 (diff)
Merge PR #13455: Fix comparison of extracted array literals
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions