diff options
| author | Gaëtan Gilbert | 2020-03-13 14:01:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-13 14:01:23 +0100 |
| commit | b6e6751011bc3ede5da75394ef2ed9396b28f87f (patch) | |
| tree | b3e18ec5f12a9c188972ace4970c6a3b51d543b4 /.github | |
| parent | 576494e2bfd925af9180f696201788534a06fd31 (diff) | |
| parent | 1c744339e54d108f5cfcadd830431a27776a658f (diff) | |
Merge PR #11016: [proof] Remove duplication in the proof save path.
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions