diff options
| author | coqbot-app[bot] | 2020-09-08 08:53:26 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-08 08:53:26 +0000 |
| commit | ebcfaf62423ee8e35167a5f4b275a17bec111180 (patch) | |
| tree | c048f73b310c105e4c2c4ca208d7e7632a680d67 /doc/plugin_tutorial | |
| parent | dde607ce50ddcf5f965d4ce222ca50f4d169a2f3 (diff) | |
| parent | f238af85799ddc727944a31064368a5bd1798365 (diff) | |
Merge PR #12927: Explain that tactics applied to multiple goals don't preserve the order
Reviewed-by: Zimmi48
Ack-by: chdoc
Ack-by: jfehrle
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions