diff options
| author | Emilio Jesus Gallego Arias | 2019-06-11 03:03:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:14 +0200 |
| commit | a0d2a039a62e26b5d87a8cd9d77f4678f2bfda4a (patch) | |
| tree | 98c43d87e826477772817d6e186f342f71a4207b /dev | |
| parent | f147f7826aad760920efa7001586aa63002847d6 (diff) | |
[proof] Respond to a comment by Pierre-Marie
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions