diff options
| author | Maxime Dénès | 2019-01-20 11:01:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-20 11:01:30 +0100 |
| commit | 051b6efe1d730afe1a08eecac71282e24c4d4523 (patch) | |
| tree | caf43bb2520bc45abc88e492133e9a49465ae399 /pretyping/arguments_renaming.ml | |
| parent | b2877df2c79147bd2e26e53e43291b9b29a2aab8 (diff) | |
| parent | 2489ef525881d875c7661d9410b9e1521013dd11 (diff) | |
Merge PR #9353: Fix merge-pr.sh when multiple review comments
Reviewed-by: maximedenes
Diffstat (limited to 'pretyping/arguments_renaming.ml')
0 files changed, 0 insertions, 0 deletions