diff options
| author | Maxime Dénès | 2016-10-12 15:15:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-12 15:15:33 +0200 |
| commit | d48176857632e1d2a0af0a31dc922f3c52047707 (patch) | |
| tree | 7d2ec99a1488a83fb6ec99c7b05e161407d2a4bf /plugins/syntax/string_syntax_plugin.mlpack | |
| parent | 6e49be2c03f11f412d17e41ca2e74232d12d915c (diff) | |
| parent | 3be2307af0f1316630b46078fd6b4367c283472d (diff) | |
Merge remote-tracking branch 'github/pr/286' into v8.5
Was PR#286: Fix the definition of if_then_else for tactics with multiple
success.
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions