diff options
| author | Maxime Dénès | 2018-02-13 11:17:00 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-13 11:17:00 +0100 |
| commit | 19d4ba5fa2ff8827f86d00df95a88e3f5cbdfd10 (patch) | |
| tree | 47b48811cca0634dfdb6df780e13b3809903e852 /interp | |
| parent | f6cc1ab4fcc26e2b0ed9186ee9a3caca7a123d97 (diff) | |
| parent | c0e99b45a97aa0d506e32d1daeb594c372ea82fa (diff) | |
Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions