diff options
| author | Maxime Dénès | 2017-06-26 21:23:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-26 21:23:29 +0200 |
| commit | d7189f0e97dae3f0de9641be3242552873040c44 (patch) | |
| tree | 6b926b426a0571f3b228f65a8c94c4c0a7e96c4e /engine/ftactic.ml | |
| parent | 4fbb431c81116b04e9c34cd7c6ffbf5d5f204f5e (diff) | |
| parent | d4a0e0bcc7689457340af5a3007a541b92e12301 (diff) | |
Merge PR#826: Put plugin exports in the right compatibility file
Diffstat (limited to 'engine/ftactic.ml')
0 files changed, 0 insertions, 0 deletions