aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorcoqbot2020-08-06 18:28:52 +0200
committerGitHub2020-08-06 18:28:52 +0200
commita5a4cbbf71863f8a4fdac32455ea6043e192fc5e (patch)
tree0ef4bf993253e01494ca35c8ba55b9d0c1c861ec /interp
parent51ecccef0308eceec1ddd9776a03fd993b3ea71a (diff)
parentddce800dbb4ed77c6839eef814da0b6e4bfe5aa4 (diff)
Merge PR #12782: Trying to rephrase complex sentences to make them easier to read.
Reviewed-by: jfehrle Ack-by: Mbodin Ack-by: corwin-of-amber
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions