diff options
| author | Tej Chajed | 2020-02-24 13:31:55 -0500 |
|---|---|---|
| committer | Tej Chajed | 2020-02-24 13:31:55 -0500 |
| commit | da984ceafbb450dc5a9fe8f8971d8c90a060f233 (patch) | |
| tree | d852c4393dc5630e7e667f5b37a481343d23fa3b /dev/ci | |
| parent | 46fe9b26ad55a266b71bbd428ee406b03a9db030 (diff) | |
| parent | 059da3541f54311283067cb3010b539506cb70bd (diff) | |
Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.
Reviewed-by: tchajed
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions