diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 18:11:51 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-30 18:11:51 +0100 |
| commit | ce12efa08f576ee2b97818a7209df328836fc638 (patch) | |
| tree | faee950920a1d810ecaf0d3a866b0acc085ec2c5 /dev/ci/docker | |
| parent | 28ea499486dd17076d8f2f4c31d7fdebeacdff8e (diff) | |
[test-suite] Test section-local mutual Fixpoint.
Noticed by coverage, test code by Gäetan Gilbert.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions