aboutsummaryrefslogtreecommitdiff
path: root/dev/include_printers
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-19 08:14:29 +0000
committerGitHub2020-10-19 08:14:29 +0000
commite6a00dd734018f6dea95dcf9c19b62f04df245e5 (patch)
treef8e5d28c24859287e86b42abb0aa3a17ee5c25db /dev/include_printers
parente583be62b74d71b5af159700e3a31f78fec9a7d2 (diff)
parent276ad0f2f2db5e4ddc569da606a6db8873fdec00 (diff)
Merge PR #13192: Fix algebraic on the right when using bidi hints
Reviewed-by: gares
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions