diff options
| author | Maxime Dénès | 2017-06-26 14:11:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-26 14:11:16 +0200 |
| commit | 4fbb431c81116b04e9c34cd7c6ffbf5d5f204f5e (patch) | |
| tree | 1ddf10b274b6ea4040fec27585333a1900e8bbae /engine/ftactic.ml | |
| parent | a579a0a0d45206f67e73273d36209fbc7bb2dddc (diff) | |
| parent | cdd6e87e0a8df4b6af4a08353f260fb035af48fb (diff) | |
Merge PR#825: Ignore all PDF files.
Diffstat (limited to 'engine/ftactic.ml')
0 files changed, 0 insertions, 0 deletions