diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-10-22 15:16:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-10-22 15:17:24 +0200 |
| commit | cb93c558cc3d30a486d45f4e4c54799e1a9c889f (patch) | |
| tree | d2c1c199ae8dfce3f7b1acc080f87274af6c7ac5 /tools | |
| parent | 21a9cec02cc389a33cf1fc0dc6d0229939abc51d (diff) | |
Fix test-suite for #2729.
Was always failing due to an incorrect use of Ltac's or.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions