diff options
| author | coqbot-app[bot] | 2020-12-15 17:44:45 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-15 17:44:45 +0000 |
| commit | c6058328a1ba583b32bdb7d2e5843a2ba1d5cf73 (patch) | |
| tree | 8e789d10d00633878b650a1550dcb9365d919633 /dev/ci | |
| parent | f78f812fcba627a913b8c044626df3642ba17c89 (diff) | |
| parent | 421ed6bb43e01a2675df2cfae286d1cfcc691fcc (diff) | |
Merge PR #13609: Extrude the computation of redexp flags in reduce.
Reviewed-by: herbelin
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions