diff options
| author | Pierre-Marie Pédrot | 2019-06-05 09:29:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-05 09:29:23 +0200 |
| commit | 658ae0d320473e25ee60cf158ed808be294f3a69 (patch) | |
| tree | 05c14bec8038c76f618c4f45e5a26ee89aaf7bb3 /.github | |
| parent | 2c6220c7973510b801d4d3c897c482b3f8c5b10d (diff) | |
| parent | 805211a603431f4ba351e0164b0bd147a771a1a0 (diff) | |
Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTEND
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions