diff options
| author | Emilio Jesus Gallego Arias | 2019-06-16 23:11:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-16 23:11:51 +0200 |
| commit | 9b7fd95b825657479d21a7231f5a6c2171f49e3e (patch) | |
| tree | 05ca9cc7af288eca2b87e99df5f69e248900c02c /doc/plugin_tutorial | |
| parent | 6eba5b5ba91f9ec02b809e0c223324e0f4fdbf85 (diff) | |
| parent | 3ca9529b5fdbb8e2a3dc18e38862cbe351e8e0e0 (diff) | |
Merge PR #10381: Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.
Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions