diff options
| author | Pierre-Marie Pédrot | 2020-02-24 18:15:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-24 18:15:04 +0100 |
| commit | 46fe9b26ad55a266b71bbd428ee406b03a9db030 (patch) | |
| tree | 7a3dfd42aa92a6b17cb7edd6a6f8df2a87219104 /gramlib | |
| parent | 00a3dcc11342e1304f078e1457dcfd118dc4e573 (diff) | |
| parent | 94fcc24a7a81253e3ede8661fc12401bbebdd14f (diff) | |
Merge PR #11653: Tactic_matching.pattern_match_term: remove ignored "refresh" argument
Reviewed-by: ppedrot
Diffstat (limited to 'gramlib')
0 files changed, 0 insertions, 0 deletions