aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorHugo Herbelin2018-12-12 14:07:12 +0100
committerHugo Herbelin2018-12-12 14:07:12 +0100
commitdfd4c4a2b50edf894a19cd50c43517e1804eadc9 (patch)
tree2e7d4477c2effb1975f7964e2a82a497b28cb3bc /checker
parent84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff)
parentcac9811632834b0135f4408a32b4a2d391d09a0d (diff)
Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions