diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-01 18:37:20 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-01 18:37:20 +0100 |
commit | 8e3aef19711fa6ccbcb2946afdb690c2fc3d900d (patch) | |
tree | 79a4de6bb4d7beb279a1dee22e215655e18a3703 /test-suite/_CoqProject | |
parent | c658141acff6d1b7f610960dd39998385c7e8806 (diff) | |
parent | 779c0bd23bbc0bd1d0c1cb358fe9725e7d7ccc74 (diff) |
Merge PR #6660: [lib] Respect change of options under with/without_option.
Diffstat (limited to 'test-suite/_CoqProject')
0 files changed, 0 insertions, 0 deletions