diff options
| author | Julien Forest | 2017-06-29 17:27:04 +0200 |
|---|---|---|
| committer | Julien Forest | 2017-06-29 17:27:04 +0200 |
| commit | 10c81e90a836c8abea32bc6157976b9adf7775fa (patch) | |
| tree | a7c4f13cacb5ea4438ba3e062f45c8fd2f15b270 /engine/ftactic.ml | |
| parent | 181cb78d09ba55c7a6d62b333b26595a4fbb360a (diff) | |
closing bug #5618 introduce by PR 828
Diffstat (limited to 'engine/ftactic.ml')
0 files changed, 0 insertions, 0 deletions