aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Zeimer <zzaimer@gmail.com>2018-07-20 18:56:43 +0200
committerGravatar Zeimer <zzaimer@gmail.com>2018-07-20 18:57:32 +0200
commitb2bdaad8567e3ca91e036268a042129b6ce6f987 (patch)
tree6880c2bf0ebbf496e374f8a1476bb59d5e615dec /theories
parent3eeb4fb840328a0f8831c402b2347196bfa0042d (diff)
Small improvements suggested in comments to PR #8086.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions